Fixed warning in decision_engine.h, minor tweak to caregraph function in

arrays, fixed bug with equalities between constants in shared terms database

1 files changed, 17 insertions, 0 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 1bb830aa8..46a9f5855 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -936,3 +936,20 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     lemma(conflict, true, false);
   }
 }
+
+
+//Conflict from shared terms database
+void TheoryEngine::sharedConflict(TNode conflict) {
+  // Mark that we are in conflict
+  d_inConflict = true;
+
+  if(Dump.isOn("t-conflicts")) {
+    Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
+                        << CheckSatCommand(conflict.toExpr());
+  }
+
+  Node fullConflict = explain(ExplainTask(d_sharedTerms.explain(conflict), SHARED_DATABASE_EXPLANATION));
+  Assert(properConflict(fullConflict));
+  Debug("theory") << "TheoryEngine::sharedConflict(" << conflict << "): " << fullConflict << std::endl;
+  lemma(fullConflict, true, false);
+}