From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 1 Mar 2022 06:02:51 +0000 (-0600)
Subject: Fix lambda lifting + proofs (#8152)
X-Git-Tag: cvc5-1.0.0~356
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca3787fc653a0024a78758f603ea2573b21d4ab2;p=cvc5.git

Fix lambda lifting + proofs (#8152)

Was leading to eager proof checking failures on proof-new.
---

diff --git a/src/theory/uf/lambda_lift.cpp b/src/theory/uf/lambda_lift.cpp
index 605e346af..01b0259b3 100644
--- a/src/theory/uf/lambda_lift.cpp
+++ b/src/theory/uf/lambda_lift.cpp
@@ -116,7 +116,15 @@ Node LambdaLift::getAssertionFor(TNode node)
     skolem_app_c.push_back(skolem);
     skolem_app_c.insert(skolem_app_c.end(), node[0].begin(), node[0].end());
     Node skolem_app = nm->mkNode(APPLY_UF, skolem_app_c);
-    children.push_back(skolem_app.eqNode(node[1]));
+    skolem_app_c[0] = node;
+    Node rhs = nm->mkNode(APPLY_UF, skolem_app_c);
+    // For the sake of proofs, we use
+    // (= (k t1 ... tn) ((lambda (x1 ... xn) s) t1 ... tn)) here. This is instead of
+    // (= (k t1 ... tn) s); the former is more accurate since
+    // beta reduction uses capture-avoiding substitution, which implies that
+    // ((lambda (y1 ... yn) s) t1 ... tn) is alpha-equivalent but not
+    // necessarily syntactical equal to s.
+    children.push_back(skolem_app.eqNode(rhs));
     // axiom defining skolem
     assertion = nm->mkNode(FORALL, children);