attempt to fix bug 293: if a split on a trivial shared pair is requested from a theor...

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e36d163a41bd5402fb9f8343a366f3891f146b96..aa897b24439a2b1d14d12cb91d11aef1583cd1aa 100644 (file)
--- 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);

diff --git a/test/regress/regress0/uflra/Makefile b/test/regress/regress0/uflra/Makefile
new file mode 100644 (file)
index 0000000..119c530
--- /dev/null
+++ b/test/regress/regress0/uflra/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/uflra
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check

diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index 7caeedbb3f8d0e02c13b5a3416b09f783ef0ebf8..bee9e8d76efc9c1152fbdd110138b5ebb1700712 100644 (file)
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -16,6 +16,7 @@ SMT_TESTS = \
        simple.02.cvc \
        simple.03.cvc \
        simple.04.cvc \
+       bug293.cvc \
        pb_real_10_0100_10_10.smt \
        pb_real_10_0100_10_11.smt \
        pb_real_10_0100_10_15.smt \

diff --git a/test/regress/regress0/uflra/bug293.cvc b/test/regress/regress0/uflra/bug293.cvc
new file mode 100644 (file)
index 0000000..3bc91c7
--- /dev/null
+++ b/test/regress/regress0/uflra/bug293.cvc
@@ -0,0 +1,8 @@
+% EXPECT: unsat
+% EXIT: 20
+x: REAL;
+f: REAL -> REAL;
+ASSERT NOT (f(1) = f(x));
+ASSERT NOT (f(0) = f(x));
+ASSERT (x = 0) XOR (x = 1);
+CHECKSAT;
\ No newline at end of file