From 7938b8dd3f7781751f8e9df3c06d0264b68e123a Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sun, 18 Jun 2017 08:54:36 -0500
Subject: Minor change to ensureTheoryAtoms for bug 828.

---
 src/theory/theory_engine.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'src/theory')

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;
-- 
cgit v1.2.3