summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2012-06-12 18:53:40 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2012-06-12 18:53:40 +0000
commitc5cdb4202b65d59aafa4156664400338958a3aa1 (patch)
tree66f407d45acfea0381046dc71c1c093fc13f2d30
parent706e3058a2a685a6849b2290f80167b74aded0be (diff)
conflicts from theories are removable
-rw-r--r--src/theory/theory_engine.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a7c378152..a047b2b06 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1137,11 +1137,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
Node fullConflict = mkExplanation(explanationVector);
Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << std::endl;
Assert(properConflict(fullConflict));
- lemma(fullConflict, true, false);
+ lemma(fullConflict, true, true);
} else {
// When only one theory, the conflict should need no processing
Assert(properConflict(conflict));
- lemma(conflict, true, false);
+ lemma(conflict, true, true);
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback