Recursive

src/rewriter/basic_rewrite_rcons.cpp

@@ -1210,6 +1210,7 @@ bool BasicRewriteRCons::ensureProofMacroQuantRewriteBody(CDProof* cdp,
 
 bool BasicRewriteRCons::ensureProofMacroLambdaAppElimShadow(CDProof* cdp,
                                                             const Node& eq)
+
 {
   Trace("brc-macro") << "Expand macro lambda app elim shadow for " << eq
                      << std::endl;
@@ -1225,15 +1226,33 @@ bool BasicRewriteRCons::ensureProofMacroLambdaAppElimShadow(CDProof* cdp,
                            "MacroLambdaAppElimShadow",
                            nullptr,
                            true);
-  for (const Node& mc : matchConds)
+  size_t i = 0;
+  while (i < matchConds.size())
   {
     Assert(mc.getKind() == Kind::EQUAL);
-    // the step should be shown by alpha-equivalance
-    tcpg.addRewriteStep(mc[0],
-                        mc[1],
-                        nullptr,
-                        true,
-                        TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE);
+    Node mc = matchConds[i];
+    i++;
+    if (mc[0].getKind() == mc[1].getKind() && mc[0].isClosure())
+    {
+      Subs s;
+      for (size_t v = 0, nvars = mc[0][0].getNumChildren(); v < nvars; v++)
+      {
+        if (mc[0][0][v] != mc[1][0][v])
+        {
+          s.add(mc[0][0][v], mc[1][0][v]);
+        }
+      }
+      Node mcr = s.apply(mc[0]);
+      Trace("brc-macro") << "- subgoal " << mc[0].eqNode(mcr) << std::endl;
+      // the step should be shown by alpha-equivalance
+      tcpg.addRewriteStep(mc[0],
+                          mcr,
+                          nullptr,
+                          true,
+                          TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE);
+      // also get match conditions in the bodies of lambdas
+      expr::getMatchConditions(mcr[1], mc[1][1], matchConds, true);
+    }
   }
   std::shared_ptr<ProofNode> pfn = tcpg.getProofForRewriting(eq[0]);
   Node res = pfn->getResult();