From 07d4adeb64dc0e00af4f239be0798023781db036 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sun, 18 Jun 2017 09:09:16 -0500
Subject: [PATCH] Fix assertion

---
 src/theory/theory_engine.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d0b714cbb..f99de0c3b 100644
--- 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;
-- 
2.30.2