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, 12 insertions, 1 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index dd642a865..faa6bbd26 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -279,6 +279,11 @@ class TheoryEngine {
   void conflict(TNode conflict, theory::TheoryId theoryId);
 
   /**
+   * Called by shared terms database to notify of a conflict.
+   */
+  void sharedConflict(TNode conflict);
+
+  /**
    * Debugging flag to ensure that shutdown() is called before the
    * destructor.
    */
@@ -353,7 +358,13 @@ class TheoryEngine {
 
   void propagateSharedLiteral(TNode literal, TNode original, theory::TheoryId theory)
   {
-    d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory));
+    if (literal.getKind() == kind::CONST_BOOLEAN) {
+      Assert(!literal.getConst<bool>());
+      sharedConflict(original);
+    }
+    else {
+      d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory));
+    }
   }
 
   /**