diff --git a/src/rewriter/rewrite_db_proof_cons.cpp b/src/rewriter/rewrite_db_proof_cons.cpp
index 445e09d15f9..75976dfb49c 100644
--- 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;