Do not eliminate variables that are equal to unevaluatable terms (#4267)

When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled.

This PR ensures we only eliminate variables when v contains only evaluated operators.

Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change.

Fixes #4500.

1 files changed, 8 insertions, 5 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 32791415e..fd8459641 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -634,13 +634,13 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
   {
     case kind::EQUAL:
     {
-      if (in[0].isVar() && !expr::hasSubterm(in[1], in[0]))
+      if (in[0].isVar() && isLegalElimination(in[0], in[1]))
       {
         ++(d_statistics.d_solveSubstitutions);
         outSubstitutions.addSubstitution(in[0], in[1]);
         return PP_ASSERT_STATUS_SOLVED;
       }
-      if (in[1].isVar() && !expr::hasSubterm(in[0], in[1]))
+      if (in[1].isVar() && isLegalElimination(in[1], in[0]))
       {
         ++(d_statistics.d_solveSubstitutions);
         outSubstitutions.addSubstitution(in[1], in[0]);
@@ -652,7 +652,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
               && node[0].isConst()))
       {
         Node extract = node[0].isConst() ? node[1] : node[0];
-        if (extract[0].getKind() == kind::VARIABLE)
+        if (extract[0].isVar())
         {
           Node c = node[0].isConst() ? node[0] : node[1];
 
@@ -688,8 +688,11 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
           }
           Node concat = utils::mkConcat(children);
           Assert(utils::getSize(concat) == utils::getSize(extract[0]));
-          outSubstitutions.addSubstitution(extract[0], concat);
-          return PP_ASSERT_STATUS_SOLVED;
+          if (isLegalElimination(extract[0], concat))
+          {
+            outSubstitutions.addSubstitution(extract[0], concat);
+            return PP_ASSERT_STATUS_SOLVED;
+          }
         }
       }
     }