4 files changed, 10 insertions, 49 deletions

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 9c24dd690..8d066c1ba 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -190,16 +190,19 @@ void Assertions::addFormula(TNode n,
   // Ensure that it does not contain free variables
   if (maybeHasFv)
   {
-    if (expr::hasFreeVar(n))
+    bool wasShadow = false;
+    if (expr::hasFreeOrShadowedVar(n, wasShadow))
     {
+      std::string varType(wasShadow ? "shadowed" : "free");
       std::stringstream se;
       if (isFunDef)
       {
-        se << "Cannot process function definition with free variable.";
+        se << "Cannot process function definition with " << varType
+           << " variable.";
       }
       else
       {
-        se << "Cannot process assertion with free variable.";
+        se << "Cannot process assertion with " << varType << " variable.";
         if (language::isLangSygus(options().base.inputLanguage))
         {
           // Common misuse of SyGuS is to use top-level assert instead of
diff --git a/src/smt/difficulty_post_processor.cpp b/src/smt/difficulty_post_processor.cpp
index 748092238..31797ba5e 100644
--- a/src/smt/difficulty_post_processor.cpp
+++ b/src/smt/difficulty_post_processor.cpp
@@ -69,7 +69,7 @@ void DifficultyPostprocessCallback::getDifficultyMap(
   NodeManager* nm = NodeManager::currentNM();
   for (const std::pair<const Node, uint64_t>& d : d_accMap)
   {
-    dmap[d.first] = nm->mkConst(Rational(d.second));
+    dmap[d.first] = nm->mkConst(CONST_RATIONAL, Rational(d.second));
   }
 }
 
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 56a759866..a292fec8f 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -855,7 +855,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
         for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi;
              j++)
         {
-          Node nodej = nm->mkConst(Rational(j));
+          Node nodej = nm->mkConst(CONST_RATIONAL, Rational(j));
           cdp->addStep(
               children[i][j], PfRule::AND_ELIM, {children[i]}, {nodej});
         }
@@ -1086,8 +1086,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       TNode child = children[i];
       TNode scalar = args[i];
       bool isPos = scalar.getConst<Rational>() > 0;
-      Node scalarCmp =
-          nm->mkNode(isPos ? GT : LT, scalar, nm->mkConst(Rational(0)));
+      Node scalarCmp = nm->mkNode(
+          isPos ? GT : LT, scalar, nm->mkConst(CONST_RATIONAL, Rational(0)));
       // (= scalarCmp true)
       Node scalarCmpOrTrue = steps.tryStep(PfRule::EVALUATE, {}, {scalarCmp});
       Assert(!scalarCmpOrTrue.isNull());
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index edf4e2761..341893a70 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -342,48 +342,6 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node,
       }
     }
   }
-  else if (node.getKind() == kind::LAMBDA)
-  {
-    // if a lambda, do lambda-lifting
-    if (!expr::hasFreeVar(node))
-    {
-      skolem = getSkolemForNode(node);
-      if (skolem.isNull())
-      {
-        Trace("rtf-proof-debug")
-            << "RemoveTermFormulas::run: make LAMBDA skolem" << std::endl;
-        // Make the skolem to represent the lambda
-        SkolemManager* sm = nodeManager->getSkolemManager();
-        skolem = sm->mkPurifySkolem(
-            node,
-            "lambdaF",
-            "a function introduced due to term-level lambda removal");
-        d_skolem_cache.insert(node, skolem);
-
-        // The new assertion
-        std::vector<Node> children;
-        // bound variable list
-        children.push_back(node[0]);
-        // body
-        std::vector<Node> skolem_app_c;
-        skolem_app_c.push_back(skolem);
-        skolem_app_c.insert(skolem_app_c.end(), node[0].begin(), node[0].end());
-        Node skolem_app = nodeManager->mkNode(kind::APPLY_UF, skolem_app_c);
-        children.push_back(skolem_app.eqNode(node[1]));
-        // axiom defining skolem
-        newAssertion = nodeManager->mkNode(kind::FORALL, children);
-
-        // Lambda lifting is trivial to justify, hence we don't set a proof
-        // generator here. In particular, replacing the skolem introduced
-        // here with its original lambda ensures the new assertion rewrites
-        // to true.
-        // For example, if (lambda y. t[y]) has skolem k, then this lemma is:
-        //   forall x. k(x)=t[x]
-        // whose witness form rewrites
-        //   forall x. (lambda y. t[y])(x)=t[x] --> forall x. t[x]=t[x] --> true
-      }
-    }
-  }
   else if (node.getKind() == kind::WITNESS)
   {
     // If a witness choice