Incorrect result from python z3-solver on MacOS-CodePudding

I am new on z3. I am trying to run the following python examples with z3.

from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(And(x y>1,x==0.00001,y==0.1))
print(s.check())

The returned result is sat, which I think is incorrect as x y=0.10001<1. I also print out the solver s

[And(x   y > 1, x == 1/0, y == 1/10)]

which I notice have term x==1/0 with a 0 in the denominator. I am using Python 3.9.8, z3-solver 4.8.12.0 running on macOS 10.14.6 Mojave.

I also tried the exact same example on a machine with Ubuntu 20.04, python3.8, and z3-solver 4.8.10.0. The returned result is unsat and there is no 0 in the denominators when the solver is printed out.

Does anyone know if I am doing anything wrong here? Thank you very much in advance.

CodePudding user response：

I cannot replicate this with z3 4.8.14; where it prints unsat, like you found with 4.8.10. You should simply upgrade your version of z3.

There has been previous questions regarding this, and it appears in certain incarnations small numbers like 0.00001 weren't being correctly translated. I suspect you're suffering from the same. See here: Why is Z3 "rounding" small reals to 1.0/0.0?

Upgrading would be the best; if you can't try the recommendation there: Instead of using 0.00001, try Q(1, 100000) instead.