Fix for equality-chaining of Booleans in SMT-LIBv2.

Thanks to David Cok for reporting this.

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 0063035ffdc76779b648fbcb4cba1212af25778e..166a695a43318006b5016bbe239457441fea2c06 100644 (file)
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -715,7 +715,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         // push children
         for(int i = top.getNumChildren() - 1; i >= 0; --i) {
           Debug("bt") << "rewriting: " << top[i] << endl;
-          worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), false));
+          worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], top.getKind() == kind::CHAIN ? parentTheory : (isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN)), false));
           //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars);
           //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
         }

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 12d7ab3974e6f3e7d9c0aced6f3f10f33574465f..fec081ca81315a3e37dfac38c924a142c22025cf 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -42,6 +42,7 @@ SMT_TESTS = \
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS = \
+       chained-equality.smt2 \
        ite2.smt2 \
        ite3.smt2 \
        ite4.smt2 \

diff --git a/test/regress/regress0/chained-equality.smt2 b/test/regress/regress0/chained-equality.smt2
new file mode 100644 (file)
index 0000000..fb3a25b
--- /dev/null
+++ b/test/regress/regress0/chained-equality.smt2
@@ -0,0 +1,10 @@
+(set-option :produce-models true)
+(set-info :status unsat)
+(set-logic QF_UF)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(declare-fun z () Bool)
+(assert (= x y z))
+(assert (not x))
+(assert z)
+(check-sat)