From 60ad84f41f846c669956205163b0ac4f3641939a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 11 Apr 2022 10:33:54 -0500 Subject: [PATCH] Remove spurious case of ppRewrite (#8596) Constants equal to constants are always rewritten to false. --- src/theory/sets/theory_sets.cpp | 7 ------- src/theory/theory.cpp | 7 ------- 2 files changed, 14 deletions(-) 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()) -- 2.30.2