Minor change to ensureTheoryAtoms for bug 828.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4d2998c6868775f4591f028e769f05980539209f..d0b714cbbeac0335b3e3466f8cc78d3bb5441a92 100644 (file)
--- 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;