Bug with int2bv and multiple scopes?

Oct 23, 2014 at 6:43 AM
Am I right that the following unexpected result when distributing connected assertions that contain int2bv to two scopes (by using push) indicates a bug?
(declare-fun x () Int)
(assert (bvugt #x05 ((_ int2bv 8) x)))
(push)
(assert (= x 6))
(check-sat)
gives SAT, although #x05 is smaller than #x06.

Without the push, i.e.
(declare-fun x () Int)
(assert (bvugt #x05 ((_ int2bv 8) x)))
(assert (= x 6))
(check-sat)
the result is UNSAT, as expected.

I could reproduce these results with the release 4.3.0 as well as with the latest version of the 'unstable' branch.

Has the wrong result when using push something to do with the note 'This function (mk_int2bv) is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.' given on http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5 ?
Coordinator
Mar 21, 2015 at 3:39 PM
Yes, this is because int2bv is uninterpreted, so the result of ((_ int2bv 8) x) is undefined. This is further complicated by the fact that int2bv reasoning is disabled by default; in this particular case we can enable it, i.e., adding
(set-option :smt.bv.enable_int2bv true)
will solve both problems as expected. Note that this option only works if the "smt" tactic is called to decide the problem, other tactics may still treat int2bv as uninterpreted. See also z3-questions-about-z3-int2bv