search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

(model_evaluator.array_equalities=false, rewriter.flat=false) Soundness issues on LIA formulas #5002

Closed muchang closed 3 years ago

muchang commented 3 years ago 
[595] % z3release small.smt2
unsat
[596] % z3-4.8.7 model_evaluator.array_equalities=false rewriter.arith_ineq_lhs=true rewriter.flat=false small.smt2
unsat
[597] % z3-4.8.8 model_evaluator.array_equalities=false rewriter.arith_ineq_lhs=true rewriter.flat=false small.smt2
sat
[598] % z3release model_evaluator.array_equalities=false rewriter.arith_ineq_lhs=true rewriter.flat=false small.smt2
sat
[599] % cat small.smt2
(assert (forall ((a Int) (b Int) (c Int)) (or (= (- a) b) (distinct (- a c) b))))
(check-sat)
[600] %

It is a regression from z3-4.8.7.

Commit: 01d5f32

muchang commented 3 years ago

(model_evaluator.array_equalities=false, rewriter.flat=false) refutation soundness issues on LIA formulas

[581] % z3release small.smt2
sat
[582] % cvc4 -q small.smt2
sat
[583] % z3release model_evaluator.array_equalities=false rewriter.flat=false small.smt2
unsat
[584] % cat small.smt2
(declare-fun a () Bool)
(assert (forall ((b Int) (c Bool) (d Int) (f Int) (e Int))
 (or (not (and (or (not (or a (= b 0))) (= d f)) (= d e) (not c))) (= f (ite c 1 e)))))
(check-sat)
[585] %

Commit: 615cafe