More

src/rewriter/basic_rewrite_rcons.cpp

@@ -1597,16 +1597,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);
-    Trace("brc-macro") << "- subgoal " << mc << std::endl;
-    // 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();

test/regress/cli/regress0/proofs/dd_int_check_rec_elim_shadow.smt2

@@ -0,0 +1,8 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun p (Int) Int)
+(define-fun i ((k Int) (a Int)) Int (p 0))
+(define-fun l ((k Int) (x Int) (s Int) (t Int)) Bool (= 0 (i k x)))
+(define-fun n ((k Int) (t Int) (x Int)) Bool (and false (l 0 0 0 0)))
+(assert (n 0 0 0))
+(check-sat)