From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sun, 18 Jun 2017 13:54:36 +0000 (-0500)
Subject: Minor change to ensureTheoryAtoms for bug 828.
X-Git-Tag: cvc5-1.0.0~5765
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7938b8dd3f7781751f8e9df3c06d0264b68e123a;p=cvc5.git

Minor change to ensureTheoryAtoms for bug 828.
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4d2998c68..d0b714cbb 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1703,11 +1703,13 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
         assertToTheory(eq.notNode(), eqNormalized.notNode(), /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
       }
       continue;
+    }else if( eqNormalized.getKind() != kind::EQUAL){
+      Assert( eqNormalized.getKind()==kind::BOOLEAN_TERM_VARIABLE );
+      // this happens for Boolean term equalities V = true that are rewritten to V, we should skip
+      //  TODO : revisit this
+      continue;
     }
 
-    Assert(eqNormalized.getKind() == kind::EQUAL);
-
-
     // If the normalization did the just flips, keep the flip
     if (eqNormalized[0] == eq[1] && eqNormalized[1] == eq[0]) {
       eq = eqNormalized;