* disallow internal uses of mkVar() (you have to mkSkolem())

* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)

1 files changed, 1 insertions, 1 deletions

diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index f22b35152..cb56c3430 100644
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -135,7 +135,7 @@ void DagificationVisitor::done(TNode node) {
     // construct the let binder
     std::stringstream ss;
     ss << d_letVarPrefix << d_letVar++;
-    Node letvar = NodeManager::currentNM()->mkVar(ss.str(), (*i).getType());
+    Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType());
 
     // apply previous substitutions to the rhs, enabling cascading LETs
     Node n = d_substitutions->apply(*i);