Weaken rewrite db failure

HanielB · Feb 29, 2024 · 7466dce · 7466dce
1 parent d7c5f2e
commit 7466dce
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/rewriter/rewrite_db_proof_cons.cpp b/src/rewriter/rewrite_db_proof_cons.cpp
@@ -74,8 +74,8 @@ bool RewriteDbProofCons::prove(CDProof* cdp,
     Trace("rpc") << "...success (basic)" << std::endl;
     return true;
   }
-  // if there are quantifiers, fail immediately
-  if (expr::hasBoundVar(a) || expr::hasBoundVar(b))
+  // if a is a quantified formula, fail immediately
+  if (a.isClosure())
   {
     Trace("rpc") << "...fail (out of scope)" << std::endl;
     return false;