From 3a3a57583fd8bd4af5c3b99b0047c9b20de38bb1 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 7 Nov 2014 10:15:41 -0500
Subject: [PATCH] Revert "Fix missing case in model postprocessor (resolves bug
 #595)."

This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.

Conflicts:
	test/regress/regress0/Makefile.am
---
 src/smt/model_postprocessor.cpp  | 39 +++-----------------------------
 src/smt/smt_engine.cpp           |  1 -
 test/regress/regress0/bug595.cvc |  7 ------
 3 files changed, 3 insertions(+), 44 deletions(-)
 delete mode 100644 test/regress/regress0/bug595.cvc

diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index c0c865b98..dd9d0a78c 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -27,15 +27,6 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
     // good to go, we have the right type
     return n;
   }
-  if(n.getKind() == kind::LAMBDA) {
-    Assert(asType.isFunction());
-    Node rhs = rewriteAs(n[1], asType[1]);
-    Node out = NodeManager::currentNM()->mkNode(kind::LAMBDA, n[0], rhs);
-    Debug("boolean-terms") << "rewrote " << n << " as " << out << std::endl;
-    Debug("boolean-terms") << "need type " << asType << endl;
-    Assert(out.getType() == asType);
-    return out;
-  }
   if(!n.isConst()) {
     // we don't handle non-const right now
     return n;
@@ -245,32 +236,8 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
                            << "- returning " << n << endl;
     d_nodes[current] = n;
   } else {
-    // 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());
-      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;
-    }
+    Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
+    // rewrite to self
+    d_nodes[current] = Node::null();
   }
 }/* ModelPostprocessor::visit() */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 921d75315..577fa7413 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3568,7 +3568,6 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec
 Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
   ModelPostprocessor mpost;
   NodeVisitor<ModelPostprocessor> visitor;
-  Debug("boolean-terms") << "postproc: visit " << node << endl;
   Node value = visitor.run(mpost, node);
   Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl;
   Node realValue = mpost.rewriteAs(value, expectedType);
diff --git a/test/regress/regress0/bug595.cvc b/test/regress/regress0/bug595.cvc
deleted file mode 100644
index c11cfb6e4..000000000
--- a/test/regress/regress0/bug595.cvc
+++ /dev/null
@@ -1,7 +0,0 @@
-% EXPECT: sat
-
-f : INT -> [# i:INT, b:INT #];
-a : INT;
-ASSERT f(a) /= (# i := 0, b := 0 #);
-
-CHECKSAT;
-- 
2.30.2