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.

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 5108e312abacdcd7e94f1066e4373ae6f7cde24f..a4b9d1ddf458bf2fedc643e598e5f41e555da18a 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -295,13 +295,15 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in,
     // 2) x is not in the term t
     // 3) x : T and t : S, then S <: T
     if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
-        && (in[1].getType()).isSubtypeOf(in[0].getType()))
+        && (in[1].getType()).isSubtypeOf(in[0].getType())
+        && in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
     {
       outSubstitutions.addSubstitution(in[0], in[1]);
       return PP_ASSERT_STATUS_SOLVED;
     }
     if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])
-        && (in[0].getType()).isSubtypeOf(in[1].getType()))
+        && (in[0].getType()).isSubtypeOf(in[1].getType())
+        && in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
     {
       outSubstitutions.addSubstitution(in[1], in[0]);
       return PP_ASSERT_STATUS_SOLVED;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 565c45eb78a00bd0dff427910feaa024dc622cd1..261f8e19c0cd08b9cc5be5ff8e7cac6171431b09 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -35,6 +35,7 @@ set(regress_0_tests
   regress0/arrays/bool-array.smt2
   regress0/arrays/bug272.minimized.smt
   regress0/arrays/bug272.smt
+  regress0/arrays/bug3020.smt2
   regress0/arrays/bug637.delta.smt2
   regress0/arrays/constarr.cvc
   regress0/arrays/constarr.smt2

diff --git a/test/regress/regress0/arrays/bug3020.smt2 b/test/regress/regress0/arrays/bug3020.smt2
new file mode 100644 (file)
index 0000000..b5a8870
--- /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)