search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

Soundness issue (assert (distinct 1.0 (^ 0.0 0.0))) #2840

Closed wintered closed 4 years ago

wintered commented 4 years ago

Consider the following formula.

(assert (distinct 1.0 (^ 0.0 0.0)))
(check-sat)

Z3 gives sat although the formula is unsatisfiable.

OS: Ubuntu 18.04 Revision: 4c09b7d

NikolajBjorner commented 4 years ago

z3 treats 0^0 as uninterpreted. As far as I can see the operator ^ isn't part of SMTLIB logics, http://smtlib.cs.uiowa.edu/logics-all.shtml.

wintered commented 4 years ago

Z3 4.8.7 gives unsat on said formula though.

NikolajBjorner commented 4 years ago

that would be unsound

NikolajBjorner commented 4 years ago

current version gives SAT. 

D:\z3\build>z3 2840.smt2
sat

D:\z3\build>z3 2840.smt2 smt.random_seed=1
sat

D:\z3\build>z3 2840.smt2 smt.random_seed=2
sat

D:\z3\build>z3 2840.smt2 smt.random_seed=3
sat

D:\z3\build>z3 2840.smt2 smt.random_seed=4
sat

D:\z3\build>z3 2840.smt2 smt.random_seed=5
sat

D:\z3\build>z3 2840.smt2 smt.random_seed=6
sat