diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-18 09:09:16 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-18 09:09:16 -0500 |
| commit | 07d4adeb64dc0e00af4f239be0798023781db036 (patch) | |
| tree | ea4ea30a99b9f60ffccce65a9689140087164c41 /src | |
| parent | 7938b8dd3f7781751f8e9df3c06d0264b68e123a (diff) | |
Fix assertion
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; |