From 1c42109395b566a0068cc3ae9067fc87ab8f8e7b Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 14 Jul 2012 21:14:39 +0000
Subject: Applying Dejan's patch for bug #369, which resolves it by adding a
 new (let..) form for each introduced binding.

---
 src/printer/smt2/smt2_printer.cpp | 24 ++++++++++--------------
 1 file changed, 10 insertions(+), 14 deletions(-)

(limited to 'src/printer')

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7fa00a6e4..640f4209c 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -46,28 +46,24 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     visitor.run(dv, n);
     const theory::SubstitutionMap& lets = dv.getLets();
     if(!lets.empty()) {
-      out << "(let (";
-      bool first = true;
-      for(theory::SubstitutionMap::const_iterator i = lets.begin();
-          i != lets.end();
-          ++i) {
-        if(!first) {
-          out << ' ';
-        } else {
-          first = false;
-        }
-        out << '(';
+      theory::SubstitutionMap::const_iterator i = lets.begin();
+      theory::SubstitutionMap::const_iterator i_end = lets.end();
+      for(; i != i_end; ++ i) {
+        out << "(let ((";
         toStream(out, (*i).second, toDepth, types);
         out << ' ';
         toStream(out, (*i).first, toDepth, types);
-        out << ')';
+        out << ")) ";
       }
-      out << ") ";
     }
     Node body = dv.getDagifiedBody();
     toStream(out, body, toDepth, types);
     if(!lets.empty()) {
-      out << ')';
+      theory::SubstitutionMap::const_iterator i = lets.begin();
+      theory::SubstitutionMap::const_iterator i_end = lets.end();
+      for(; i != i_end; ++ i) {
+        out << ")";
+      }
     }
   } else {
     toStream(out, n, toDepth, types);
-- 
cgit v1.2.3