Fix assertion

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d0b714cbbeac0335b3e3466f8cc78d3bb5441a92..f99de0c3b381fd1601f61d209655a6d3b82a0353 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1704,7 +1704,8 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
       }
       continue;
     }else if( eqNormalized.getKind() != kind::EQUAL){
-      Assert( eqNormalized.getKind()==kind::BOOLEAN_TERM_VARIABLE );
+      Assert( eqNormalized.getKind()==kind::BOOLEAN_TERM_VARIABLE || 
+              ( eqNormalized.getKind()==kind::NOT && eqNormalized[0].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;