Fix a tuple attribute bug that was causing model-generation problems for tuples

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 59d23c6ea622d30dd1d86666db780e0ffa83dfc9..a3c9681582006bad4421ab588264b926670b62c2 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -412,6 +412,7 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
       dt.addConstructor(c);
       dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
       Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
+      dtt.setAttribute(DatatypeTupleAttr(), t);
     } else {
       const Record& rec = t.getRecord();
       Datatype dt("__cvc4_record");
@@ -422,8 +423,8 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
       dt.addConstructor(c);
       dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
       Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
+      dtt.setAttribute(DatatypeRecordAttr(), t);
     }
-    dtt.setAttribute(DatatypeRecordAttr(), t);
   } else {
     Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl;
   }

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 58bd6711df72b967920047a32c8476970e33d859..08b00a309d7a12cbc4cecf559a4539a5ad21c6b5 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -18,6 +18,7 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 TESTS =        \
        tuple.cvc \
+       tuple-model.cvc \
        rec1.cvc \
        rec2.cvc \
        rec4.cvc \

diff --git a/test/regress/regress0/datatypes/tuple-model.cvc b/test/regress/regress0/datatypes/tuple-model.cvc
new file mode 100644 (file)
index 0000000..2ba9671
--- /dev/null
+++ b/test/regress/regress0/datatypes/tuple-model.cvc
@@ -0,0 +1,6 @@
+% This was breaking with --check-models due to tuple model breakage.
+% EXPECT: sat
+% EXIT: 10
+x : [ INT, INT ];
+ASSERT x.0 = 5;
+CHECKSAT;