From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 17 May 2013 15:12:36 +0000 (-0400)
Subject: Fix for equality-chaining of Booleans in SMT-LIBv2.
X-Git-Tag: cvc5-1.0.0~7287^2~113^2~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=41c388ad28f54fbd27fd954bc1486453dcbf1e84;p=cvc5.git

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 0063035ff..166a695a4 100644
--- 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 12d7ab397..fec081ca8 100644
--- 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
index 000000000..fb3a25b94
--- /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)