Remove spurious case of ppRewrite (#8596)

Constants equal to constants are always rewritten to false.

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 848459171af234e6c2d2455fa2ff7a533ac9a3f6..454a86a73cbf6d4a5ca34f2b50f1e04378343235 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -191,13 +191,6 @@ Theory::PPAssertStatus TheorySets::ppAssert(
         status = Theory::PP_ASSERT_STATUS_SOLVED;
       }
     }
-    else if (in[0].isConst() && in[1].isConst())
-    {
-      if (in[0] != in[1])
-      {
-        status = Theory::PP_ASSERT_STATUS_CONFLICT;
-      }
-    }
   }
   return status;
 }

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 05613963b06cf3da6566155359c011f4b10acfb4..a6e16e855fb62a580f1772d4983122d7267ce4ff 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -459,13 +459,6 @@ Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
       outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
       return PP_ASSERT_STATUS_SOLVED;
     }
-    if (in[0].isConst() && in[1].isConst())
-    {
-      if (in[0] != in[1])
-      {
-        return PP_ASSERT_STATUS_CONFLICT;
-      }
-    }
   }
   else if (in.getKind() == kind::NOT && in[0].getKind() == kind::EQUAL
            && in[0][0].getType().isBoolean())