From f65fd6a5150436a6defbe00acbcdca08d94e9cd6 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 24 May 2019 23:38:46 -0700
Subject: Avoid substituting Boolean term variables

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.
---
 src/theory/theory.cpp                     |  6 ++++--
 test/regress/CMakeLists.txt               |  1 +
 test/regress/regress0/arrays/bug3020.smt2 | 16 ++++++++++++++++
 3 files changed, 21 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress0/arrays/bug3020.smt2

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 5108e312a..a4b9d1ddf 100644
--- 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 c920f21a9..0b8e74926 100644
--- 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
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)
-- 
cgit v1.2.3