diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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; |