diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-05-27 16:36:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-05-27 16:36:17 -0700 |
commit | 60173f62a82b4d71f2fbac51880d44d883ae5109 (patch) | |
tree | 7063c98d4da6405545ffe25ca3962f222fcebe12 /test/regress/regress0 | |
parent | 1c1c178db1755a441792d84465dcb8397f1f2011 (diff) |
Avoid substituting Boolean term variables (#3022)
Fixes #3020. Boolean terms that appear in other terms, e.g. a Boolean
array index, are replaced by `BOOLEAN_TERM_VARIABLE`s to make sure that
they are handled properly in theory combination. When doing this
replacement, an equality of the form `(= <Boolean term> <Boolean term
variable)` is added to the assertions. The problem was that
`Theory::ppAssert()` would derive a substitution when this equality was
registered. The commit fixes the problem by not allowing to add
substitutions for `BOOLEAN_TERM_VARIABLE`s.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/arrays/bug3020.smt2 | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress0/arrays/bug3020.smt2 b/test/regress/regress0/arrays/bug3020.smt2 new file mode 100644 index 000000000..b5a88700b --- /dev/null +++ b/test/regress/regress0/arrays/bug3020.smt2 @@ -0,0 +1,16 @@ +(set-info :status sat) +(set-logic QF_ABV) +(declare-const A (Array Bool Bool)) +(declare-const B (Array Bool Bool)) +(declare-const b1 Bool) +(declare-const b2 Bool) +(declare-const b3 Bool) +(declare-const b4 Bool) +(assert (= A (store B b1 b2))) +(assert (= b3 (select A (select B b2)))) +(assert (=> b1 b2)) +(assert (not (and b2 b3))) +(assert (=> b3 b1)) +(assert (= b4 (select B b2))) +(assert (xor b4 b2)) +(check-sat) |