From 19abe15ccc1e310ae3f726b351b0023670ba7962 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 14 Nov 2012 23:49:07 +0000
Subject: Fix for bug 407. mkAnonymousFunction() in the parser no longer uses
 ':'. CVC printer now properly prints LAMBDAs. Model builing now gives bound
 variables names that can be parsed bypresentation language.

---
 src/printer/cvc/cvc_printer.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'src/printer/cvc')

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 4fc94947b..14347ff8e 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -212,8 +212,12 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       // no-op
       break;
     case kind::LAMBDA:
-      op << "LAMBDA";
-      opType = PREFIX;
+      out << "(LAMBDA";
+      toStream(out, n[0], depth, types, true);
+      out << ": ";
+      toStream(out, n[1], depth, types, true);
+      out << ")";
+      return;
       break;
     case kind::APPLY:
       toStream(op, n.getOperator(), depth, types, true);
-- 
cgit v1.2.3