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 605e346af5a885e773373b080589acc82d5085f3..01b0259b3f72b06e93029dd9ebbed5c1590f7313 100644 (file)
--- 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);