search

Z3Prover / z3

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

Invalid model for ALL formulas (smt.arith.solver 1) #4229

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula

(set-logic ALL)
(set-option :model_validate true)
(set-option :smt.arith.solver 1)
(declare-const r0 Real)
(declare-const r4 Real)
(push 1)
(assert (not (forall ((q44 (_ BitVec 12)) (q45 Int)) (>= q45 0))))
(assert (distinct r0 (* 666550.0 r4 666550.0 r4)))
(push 1)
(pop 1)
(check-sat)

z3 (commit 1f15033ca) gives an invalid model

rainoftime commented 4 years ago 
(set-logic ALL)
(declare-fun _substvar_62_ () (Array Bool (_ BitVec 8)))
(declare-fun _substvar_63_ () Bool)
(set-option :model_validate true)
(set-option :smt.arith.solver 1)
(declare-const v7 Bool)
(declare-const i1 Int)
(push 1)
(assert (exists ((q13 (Array (Array Bool (_ BitVec 8)) Bool)) (q14 (_ BitVec 8)) (q15 Int) (q16 (Array Bool (_ BitVec 8))) (q17 Real) (q18 (Array Real (Array Bool (_ BitVec 8)))) (q19 (Array (Array Bool (_ BitVec 8)) Bool)) (q20 (Array Bool (_ BitVec 8))) (q21 Int)) (xor (bvsge (select (store _substvar_62_ v7 #b01110000) true) (_ bv0 8)) (= q13 q13 q13 q19 q19) (distinct (+ (div 1 (* i1 91 69 69)) i1 91 1) 69))))
(assert _substvar_63_)
(assert (not (forall ((q22 Real) (q23 Real) (q24 Real)) (<= q22 0.0 0.0))))
(push 1)
(pop 1)
(check-sat)
NikolajBjorner commented 4 years ago

see warning: it is outside the fragment for difference logic