During a project, I encountered a phenomenon I can't explain. It is boiled down in the following minimal example (using Z3Py) which should be unsat but returns a model.
from z3 import *
solver = Solver()
x = Int("x")
# The next proposition is clearly unsatisfiable
solver.add(And(x > 0, (x + 1) * (1 / (x + 1)) != 1))
solver.add(x == 1)
# Still, Z3 provides a "model"
print(solver.check())
print(solver.model())
Is there anything I am missing? Is it forbidden to use division in certain situations?
Z3 version: 4.8.14 Python version: 3.9
Note that when you use / over integers, than the result is an integer itself. That is, we use integer division; which in SMTLib is defined to be the Euclidian one. See https://smtlib.cs.uiowa.edu/theories-Ints.shtml for details.
This means that the expression 1 / (1+1) reduces to 0, since division produces an integer. So you end up with 0 != 1, which is true, and thus your problem is satisfiable.
If you want division to produce reals, then you should either start with a real x (i.e., x = Real("x")) in which case your problem will be unsat; or convert the arguments to be over the reals, via an expression of the form ToReal(x); which again will produce unsat for your problem.
So, in the first case, your modification will be:
x = Real('x')
casting the problem over reals. Or, if you want to keep x an integer, yet the division to be over the reals, you should use:
solver.add(And(x > 0, ToReal(x + 1) * (1 / ToReal(x + 1)) != 1))
which does the conversion.
I should note that mixing integers and reals in this way can lead to hard problems in general, and the solver might end up reporting unknown. But that's besides the point for your particular question here.