attempt to fix bug 293: if a split on a trivial shared pair is requested from a theory, such as 1 = 0, it is reasserted to the theory.

1 files changed, 9 insertions, 2 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e36d163a4..aa897b244 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -230,11 +230,18 @@ void TheoryEngine::combineTheories() {
 
     Node equality = carePair.a.eqNode(carePair.b);
     Node normalizedEquality = Rewriter::rewrite(equality);
+	bool isTrivial = normalizedEquality.getKind() == kind::CONST_BOOLEAN;
+
 
     // If the node has a literal, it has been asserted so we should just check it
     bool value;
-    if (d_propEngine->isSatLiteral(normalizedEquality) && d_propEngine->hasValue(normalizedEquality, value)) {
-      Debug("sharing") << "TheoryEngine::combineTheories(): has a literal " << std::endl;
+    if (isTrivial || (d_propEngine->isSatLiteral(normalizedEquality) && d_propEngine->hasValue(normalizedEquality, value))) {
+      Debug("sharing") << "TheoryEngine::combineTheories(): has a literal or is trivial" << std::endl;
+
+	  if (isTrivial) {
+	    // if the equality is trivial, we assert it back to the theory saying the sat solver should explain
+	    value = normalizedEquality.getConst<bool>();
+	  }
 
       // Normalize the equality to the theory that requested it
       Node toAssert = Rewriter::rewriteEquality(carePair.theory, equality);