Avoid substituting Boolean term variablesfix3020

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.

1 files changed, 4 insertions, 2 deletions

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;