diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-18 08:54:36 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-18 08:54:36 -0500 |
commit | 7938b8dd3f7781751f8e9df3c06d0264b68e123a (patch) | |
tree | 28a26ff18e6f7387eaaa53ac516bd844aa6b00a6 /src | |
parent | 41f51ad4b0093611fa022629b15f1012a376f8e9 (diff) |
Minor change to ensureTheoryAtoms for bug 828.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory_engine.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4d2998c68..d0b714cbb 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1703,11 +1703,13 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The assertToTheory(eq.notNode(), eqNormalized.notNode(), /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER); } continue; + }else if( eqNormalized.getKind() != kind::EQUAL){ + Assert( eqNormalized.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; } - Assert(eqNormalized.getKind() == kind::EQUAL); - - // If the normalization did the just flips, keep the flip if (eqNormalized[0] == eq[1] && eqNormalized[1] == eq[0]) { eq = eqNormalized; |