Update to consistent policy for removed terms in quantifier bodies. (#4602)

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 1ae125e0319d54ad46ca1b8b7042428b0e6254c9..c3f0fabc4acd45f6caeb2e710e7d974368ec7f11 100644 (file)
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -89,8 +89,8 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
   if (node.getKind() == kind::ITE && !nodeType.isBoolean())
   {
     // Here, we eliminate the ITE if we are not Boolean and if we do not contain
-    // a bound variable.
-    if (!inQuant || !expr::hasBoundVar(node))
+    // a free variable.
+    if (!inQuant || !expr::hasFreeVar(node))
     {
       skolem = getSkolemForNode(node);
       if (skolem.isNull())
@@ -111,7 +111,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
   else if (node.getKind() == kind::LAMBDA)
   {
     // if a lambda, do lambda-lifting
-    if (!inQuant)
+    if (!inQuant || !expr::hasFreeVar(node))
     {
       skolem = getSkolemForNode(node);
       if (skolem.isNull())
@@ -143,7 +143,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
     // If a witness choice
     //   For details on this operator, see
     //   http://planetmath.org/hilbertsvarepsilonoperator.
-    if (!inQuant)
+    if (!inQuant || !expr::hasFreeVar(node))
     {
       skolem = getSkolemForNode(node);
       if (skolem.isNull())