1 files changed, 20 insertions, 6 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 005a23378..a8cbb4742 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -25,6 +25,7 @@
 #include "proof/cnf_proof.h"
 #include "proof/lfsc_proof_printer.h"
 #include "proof/proof_utils.h"
+#include "proof/quantifiers_proof.h"
 #include "proof/resolution_bitvector_proof.h"
 #include "proof/sat_proof_implementation.h"
 #include "proof/theory_proof.h"
@@ -136,6 +137,14 @@ ArithProof* ProofManager::getArithProof() {
   return (ArithProof*)pf;
 }
 
+QuantifiersProof* ProofManager::getQuantifiersProof()
+{
+  Assert(options::proof());
+  TheoryProof* pf =
+      getTheoryProofEngine()->getTheoryProof(theory::THEORY_QUANTIFIERS);
+  return (QuantifiersProof*)pf;
+}
+
 SkolemizationManager* ProofManager::getSkolemizationManager() {
   Assert (options::proof() || options::unsatCores());
   return &(currentPM()->d_skolemizationManager);
@@ -1049,12 +1058,17 @@ void ProofManager::printGlobalLetMap(std::set<Node>& atoms,
   for (unsigned i = 0; i < letOrder.size(); ++i) {
     Expr currentExpr = letOrder[i].expr;
     unsigned letId = letOrder[i].id;
-    ProofLetMap::iterator it = letMap.find(currentExpr);
-    Assert(it != letMap.end());
-    out << "\n(@ let" << letId << " ";
-    d_theoryProof->printBoundTerm(currentExpr, out, letMap);
-    paren << ")";
-    it->second.increment();
+    // TODO: BOUND_VAR_LIST should probably not be filtered out here but not
+    // even appear in the letMap in the first place.
+    if (currentExpr.getKind() != kind::BOUND_VAR_LIST)
+    {
+      ProofLetMap::iterator it = letMap.find(currentExpr);
+      Assert(it != letMap.end());
+      out << "\n(@ let" << letId << " ";
+      d_theoryProof->printBoundTerm(currentExpr, out, letMap);
+      paren << ")";
+      it->second.increment();
+    }
   }
 
   out << std::endl << std::endl;