From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 12 Jun 2020 23:30:19 +0000 (-0500)
Subject: Update to consistent policy for removed terms in quantifier bodies. (#4602)
X-Git-Tag: cvc5-1.0.0~3220
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=08f6f8cc6118b1e6c057a294d1ddb60e2e45b5ed;p=cvc5.git

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 1ae125e03..c3f0fabc4 100644
--- 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())