Another fix

ajreynol · Dec 17, 2024 · 2e46dea · 2e46dea
1 parent 499faf1
commit 2e46dea
Showing 1 changed file with 9 additions and 1 deletion.
diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp
@@ -1164,7 +1164,15 @@ bool BasicRewriteRCons::ensureProofMacroQuantRewriteBody(CDProof* cdp,
                      << std::endl;
   // Call the utility again with proof tracking and construct the term
   // conversion proof. This proof itself may have trust steps in it.
-  TConvProofGenerator tcpg(d_env, nullptr);
+  // We ensure the proof generator does not rewrite in the pattern list using a
+  // term context.
+  WithinKindTermContext wktc(Kind::INST_PATTERN_LIST);
+  TConvProofGenerator tcpg(d_env,
+            nullptr,
+            TConvPolicy::FIXPOINT,
+            TConvCachePolicy::NEVER,
+            "EnsureProofMacroQuantRewrite",
+            &wktc);
   theory::quantifiers::QuantifiersRewriter qrew(
       nodeManager(), d_env.getRewriter(), options());
   Node qr = qrew.computeRewriteBody(eq[0], &tcpg);