diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-06-16 09:06:34 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-16 09:06:34 -0700 |
| commit | 5f144347482d8ef5ee1462d0ee6fd2e293184b58 (patch) | |
| tree | dde5801f3b2241618c0b2033bea207961fb7f4aa /test/regress/regress0/bv | |
| parent | e5f880a7bb603734a737e026ba64c035b0517468 (diff) | |
BV: Fix querying equality status in lazy bit-blaster. (#4618)
Fixes #4076.
In the lazy bit-blaster, when querying the equality status, if the SAT
solver has a full model, it is queried for the model values of the
operands of the equality. However, the check if the bit-blaster has a
full model did not consider the case where no assertions have yet been
added, which leads to querying values of bits that are still unassigned
in the SAT solver.
Co-authored-by: <mathias.preiner@gmail.com>
Diffstat (limited to 'test/regress/regress0/bv')
| -rw-r--r-- | test/regress/regress0/bv/issue-4076.smt2 | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/issue-4076.smt2 b/test/regress/regress0/bv/issue-4076.smt2 new file mode 100644 index 000000000..3a80dc5f0 --- /dev/null +++ b/test/regress/regress0/bv/issue-4076.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic ALL) +(set-option :produce-models true) +(declare-fun a ((_ BitVec 2)) Int) +(declare-fun b (Int) (_ BitVec 2)) +(declare-const c Int) +(declare-const d Int) +(assert (= (a #b01) 1)) +(assert(= 0 (a (bvlshr (b c) (b d))))) +(push) +(check-sat) +(pop) +(check-sat) |