Merge branch '1.4.x'

Conflicts:
	src/smt/model_postprocessor.cpp

3 files changed, 47 insertions, 1 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 6ce8efef9..29caa92b3 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -282,11 +282,13 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw(
         const Datatype& newD = newDtt.getDatatype();
         for(c = dt.begin(); c != dt.end(); ++c) {
           Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl;
-          Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr?
+          const DatatypeConstructor *newC;
+          Node::fromExpr((*(newC = &newD[(*c).getName() + "'"])).getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr?
           Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl;
           d_varCache[Node::fromExpr((*c).getConstructor())] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
           d_varCache[Node::fromExpr((*c).getTester())] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
           for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
+            Node::fromExpr((*newC)[(*a).getName() + "'"].getSelector()).setAttribute(BooleanTermAttr(), Node::fromExpr((*a).getSelector()));// other attr?
             d_varCache[Node::fromExpr((*a).getSelector())] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
           }
         }
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index dd9d0a78c..db0ce3487 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -235,6 +235,43 @@ 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) {
+    // rewrite based on children
+    bool self = true;
+    for(size_t i = 0; i < current.getNumChildren(); ++i) {
+      Assert(d_nodes.find(current[i]) != d_nodes.end());
+      if(!d_nodes[current[i]].isNull()) {
+        self = false;
+        break;
+      }
+    }
+    if(self) {
+      Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
+      // rewrite to self
+      d_nodes[current] = Node::null();
+    } else {
+      // rewrite based on children
+      NodeBuilder<> nb(current.getKind());
+      if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        TNode op = current.getOperator();
+        Node realOp;
+        if(op.getAttribute(BooleanTermAttr(), realOp)) {
+          nb << realOp;
+        } else {
+          nb << op;
+        }
+      }
+      for(size_t i = 0; i < current.getNumChildren(); ++i) {
+        Assert(d_nodes.find(current[i]) != d_nodes.end());
+        TNode rw = d_nodes[current[i]];
+        if(rw.isNull()) {
+          rw = current[i];
+        }
+        nb << rw;
+      }
+      d_nodes[current] = nb;
+      Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << endl;
+    }
   } else {
     Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
     // rewrite to self
diff --git a/test/regress/regress0/bug595.cvc b/test/regress/regress0/bug595.cvc
new file mode 100644
index 000000000..c11cfb6e4
--- /dev/null
+++ b/test/regress/regress0/bug595.cvc
@@ -0,0 +1,7 @@
+% EXPECT: sat
+
+f : INT -> [# i:INT, b:INT #];
+a : INT;
+ASSERT f(a) /= (# i := 0, b := 0 #);
+
+CHECKSAT;