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.

1 files changed, 6 insertions, 2 deletions

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);