Bug in check-sat-assuming

[georgerennie]

I have the following example minimised from some BMC work where the presence of a check-sat-assuming call is changing the result of a following check-sat call.

(set-option :produce-models true)
(set-logic QF_UFBV)

(declare-sort State 0)
(declare-fun a (State) Bool)
(declare-fun b (State) Bool)
(declare-fun c (State) (_ BitVec 1))

(declare-const s0 State)

(assert (bvult (c s0) #b1))
(assert (distinct (c s0) #b0))

(declare-const s1 State)
(define-fun s1-eq () Bool (= (a s1) (b s1)))

(check-sat-assuming (s1-eq))
(check-sat)
(get-value ((c s0)))

Yices produces

unsat
sat
(((c s0) #b0))

Whereas z3 produces (as expected)

unsat
unsat
(error "line 19 column 19: model is not available")

This is for a build of yices taken straight from the latest commit on this repo, run with yices-smt2 --incremental bug.smt2

$ yices-smt2 --version
Yices 2.6.4
Copyright SRI International.
Linked with GMP 6.2.1
Copyright Free Software Foundation, Inc.
Build date: 2023-03-18
Platform: x86_64-pc-linux-gnu (release)
Revision: ae6aa42219c7aa260a5056564c1a76911261f0ef

[ahmed-irfan]

Thanks for reporting the issue.

I am able to reproduce the issue. We will look into this soon.