From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 11 Apr 2022 15:33:54 +0000 (-0500)
Subject: Remove spurious case of ppRewrite (#8596)
X-Git-Tag: cvc5-1.0.1~277
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=60ad84f41f846c669956205163b0ac4f3641939a;p=cvc5.git

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 848459171..454a86a73 100644
--- 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 05613963b..a6e16e855 100644
--- 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())