Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index ba7902d3235e5a14299723589ce3dfced5ca1d77..bcacd4bd48d21c48c6808ac854f003cfea277998 100644 (file)
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -706,7 +706,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         goto next_worklist;
       }
       switch(k) {
-      case kind::INST_ATTRIBUTE:
+      //case kind::INST_ATTRIBUTE:
       case kind::BOUND_VAR_LIST:
         result.top() << top;
         worklist.pop();
@@ -819,7 +819,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], top.getKind() == kind::CHAIN ? parentTheory : (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) || top.getKind()==kind::INST_ATTRIBUTE) ? 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/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index d734a6b956beae5c13ec21dc56173b3339141f75..218dde7d425fa6aa8f12a9b3c15e24a91202acb9 100644 (file)
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -62,7 +62,8 @@ TESTS =       \
        fmf-strange-bounds.smt2 \
        fmf-strange-bounds-2.smt2 \
        fmf-bound-2dim.smt2 \
-       memory_model-R_cpp-dd.cvc
+       memory_model-R_cpp-dd.cvc \
+       bug764.smt2
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/fmf/bug764.smt2 b/test/regress/regress0/fmf/bug764.smt2
new file mode 100644 (file)
index 0000000..d030c3e
--- /dev/null
+++ b/test/regress/regress0/fmf/bug764.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+
+(define-fun BoolToString ((b Bool)) String (ite b "true" "false") )
+
+(declare-datatypes () (
+    (Color (red) (white) (blue))
+) )
+
+(define-fun ColorToString ((c Color)) String (ite (is-red c) "red" (ite (is-white c) "white" "blue")) )
+
+(declare-datatypes () (
+    (CP (cp (b Bool) (c Color)))
+) )
+
+(define-fun-rec CPToString ((cp CP)) String (str.++ "cp(" (BoolToString (b cp)) "," (ColorToString (c cp)) ")"))
+
+(declare-fun CPFromString (String) CP)
+
+(assert (forall ((cp1 CP)) (= cp1 (CPFromString (CPToString cp1)))))
+
+(declare-fun cpx() CP)
+(assert (= cpx (CPFromString "cp(true,white)")))
+
+(check-sat)
+