From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sun, 18 Jun 2017 14:09:16 +0000 (-0500)
Subject: Fix assertion
X-Git-Tag: cvc5-1.0.0~5764
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=07d4adeb64dc0e00af4f239be0798023781db036;p=cvc5.git

Fix assertion
---

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;