search

Z3Prover / z3

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

Invalid model for QF_LRA formula (unsat_core) #3979

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic QF_LRA)
(declare-fun _substvar_38_ () Real)
(set-option :model_validate true)
(set-option :unsat_core true)
(declare-const r4 Real)
(declare-const v4 Bool)
(declare-const v44 Bool)
(assert (! (< (* (/ 0.0 0.0) _substvar_38_) (/ r4 0.0)) :named IP_67))
(check-sat-assuming ((! (or v4 v44 v44) :named IP_1) (! (or v4 v44) :named IP_2)))

z3 (commit dde0c514fa) gives an invalid model

zhendongsu commented 4 years ago

See Nikolaj's comment for https://github.com/Z3Prover/z3/issues/3902

rainoftime commented 4 years ago

@zhendongsu :lblpos and :named are different. The former one is introduced by Boogie, but :named is general in smt-lib2 (also supported by OpenSMT, etc)

rainoftime commented 4 years ago

There is a document http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r12.09.09.pdf (Page 25)

zhendongsu commented 4 years ago

Okay, I see; thanks. Let's see what Nikolaj says about Z3's support regarding this.

NikolajBjorner commented 4 years ago

the bug was not directly tied to named assumptions, but perhaps not too easy to trigger because it required that the variable used in division wasn't used elsewhere in arithmetical context.

NikolajBjorner commented 4 years ago

The construct :named is supported for the standard.

The constructs :lblpos :lblneg is a "Rustan" feature. It was added in 2007 and never really touched. They may have sound denotational meanings, but the implementation is very narrowly tuned to Boogie use case. I am not willing to risk breaking Boogie uses because the z3 implementation of lblpos/lblneg is highly operational.