4 files changed, 28 insertions, 5 deletions

diff --git a/src/printer/let_binding.cpp b/src/printer/let_binding.cpp
index 9f26d3800..ca3ab40f6 100644
--- a/src/printer/let_binding.cpp
+++ b/src/printer/let_binding.cpp
@@ -57,7 +57,7 @@ void LetBinding::letify(std::vector<Node>& letList)
   // populate the d_letList and d_letMap
   convertCountToLet();
   // add the new entries to the letList
-letList.insert(letList.end(), d_letList.begin() + prevSize, d_letList.end());
+  letList.insert(letList.end(), d_letList.begin() + prevSize, d_letList.end());
 }
 
 void LetBinding::pushScope() { d_context.push(); }
@@ -103,6 +103,11 @@ Node LetBinding::convert(Node n, const std::string& prefix, bool letTop) const
         ss << prefix << id;
         visited[cur] = nm->mkBoundVar(ss.str(), cur.getType());
       }
+      else if (cur.isClosure())
+      {
+        // do not convert beneath quantifiers
+        visited[cur] = cur;
+      }
       else
       {
         visited[cur] = Node::null();
diff --git a/src/printer/let_binding.h b/src/printer/let_binding.h
index e14740b61..83f3183ca 100644
--- a/src/printer/let_binding.h
+++ b/src/printer/let_binding.h
@@ -69,6 +69,19 @@ namespace CVC4 {
  * d_letList[i] does not contain subterm d_letList[j] for j>i.
  * It is intended that d_letList contains only unique nodes. Each node
  * in d_letList is mapped to a unique identifier in d_letMap.
+ *
+ * Notice that this class will *not* use introduced let symbols when converting
+ * the bodies of quantified formulas. Consider the formula:
+ * (let ((Q (forall ((x Int)) (= x (+ a a))))) (and (= (+ a a) (+ a a)) Q Q))
+ * where "let" above is from the user. When this is letified by this class,
+ * note that (+ a a) occurs as a subterm of Q, however it is not seen until
+ * after we have seen Q twice, since we traverse in reverse topological order.
+ * Since we do not traverse underneath quantified formulas, this means that Q
+ * may be marked as a term-to-letify before (+ a a), which leads to violation
+ * of the above invariant concerning containment. Thus, when converting, if
+ * a let symbol is introduced for (+ a a), we will not replace the occurence
+ * of (+ a a) within Q. Instead, the user of this class is responsible for
+ * letifying the bodies of quantified formulas independently.
  */
 class LetBinding
 {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7a27794e6..e1a4058e8 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -931,17 +931,22 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::WITNESS:
   {
     out << smtKindString(k, d_variant) << " ";
-    toStream(out, n[0], toDepth, lbind);
+    // do not letify the bound variable list
+    toStream(out, n[0], toDepth, nullptr);
     out << " ";
     if (n.getNumChildren() == 3)
     {
       out << "(! ";
     }
-    toStreamWithLetify(out, n[1], toDepth - 1, lbind);
+    // Use a fresh let binder, since using existing let symbols may violate
+    // scoping issues for let-bound variables, see explanation in let_binding.h.
+    size_t dag = lbind == nullptr ? 0 : lbind->getThreshold()-1;
+    toStream(out, n[1], toDepth - 1, dag);
     if (n.getNumChildren() == 3)
     {
       out << " ";
-      toStream(out, n[2], toDepth, lbind);
+      // do not letify the annotation
+      toStream(out, n[2], toDepth, nullptr);
       out << ")";
     }
     out << ")";
diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2
index 14f2316a7..02eb3376a 100644
--- a/test/regress/regress0/printer/let_shadowing.smt2
+++ b/test/regress/regress0/printer/let_shadowing.smt2
@@ -3,7 +3,7 @@
 ; SCRUBBER: grep assert
 ; EXPECT: (assert (let ((_let_1 (* x y))) (and (= _let_1 _let_1) (= _let_1 _let_0))))
 ; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((_let_0 Int)) (= 0 _let_0))))))
-; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_2 (and b a))) (and _let_1 _let_2 _let_2 (= 0 _let_0)))))))))
+; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_1 (and b a))) (and (and a b) _let_1 _let_1 (= 0 _let_0)))))))))
 (set-logic NIA)
 (declare-const _let_0 Int)
 (declare-const x Int)