Fix bugs 605 and 667.

1 files changed, 15 insertions, 4 deletions

diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 44b56fdd4..485b2c9a9 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -97,6 +97,15 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
     Node val = rewriteAs(asa.getExpr(), asType[1]);
     return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr()));
   }
+  if( n.getType().isSet() ){
+    if( n.getKind()==kind::UNION ){
+      std::vector< Node > children;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        children.push_back( rewriteAs( n[i], asType ) );
+      }
+      return NodeManager::currentNM()->mkNode(kind::UNION,children);
+    }
+  }
   if(n.getType().isParametricDatatype() &&
      n.getType().isInstantiatedDatatype() &&
      asType.isParametricDatatype() &&
@@ -171,7 +180,7 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     }
     Assert(t == expectType.end());
     d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << endl;
+    Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
     // The assert below is too strong---we might be returning a model value but
     // expect a type that still uses datatypes for tuples/records.  If it's
     // really not the right type we should catch it in SmtEngine anyway.
@@ -205,7 +214,7 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     }
     Assert(t == expectRec.end());
     d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << endl;
+    Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
     Assert(d_nodes[current].getType() == expectType);
   } else if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
             ( current.getOperator().hasAttribute(BooleanTermAttr()) ||
@@ -244,7 +253,9 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     Debug("boolean-terms") << "model-post: " << current << endl
                            << "- returning " << n << endl;
     d_nodes[current] = n;
-  } else if(current.getKind() == kind::LAMBDA) {
+  //all kinds with children that can occur in nodes in a model go here
+  } else if(current.getKind() == kind::LAMBDA || current.getKind() == kind::SINGLETON || current.getKind() == kind::UNION || 
+            current.getKind()==kind::STORE || current.getKind()==kind::STORE_ALL || current.getKind()==kind::APPLY_CONSTRUCTOR ) {
     // rewrite based on children
     bool self = true;
     for(size_t i = 0; i < current.getNumChildren(); ++i) {
@@ -279,7 +290,7 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
         nb << rw;
       }
       d_nodes[current] = nb;
-      Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << endl;
+      Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
     }
   } else {
     Debug("tuprec") << "returning self for kind " << current.getKind() << endl;