From 9732169b040f7f85c5b11854e5ed30bff5ca013c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 5 Sep 2022 13:44:16 -0700
Subject: [PATCH] #6320

---
 src/ast/ast.cpp | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index f60512e63..38f4dcf05 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -3027,11 +3027,23 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
             found_complement = true;
         }
     }
+    // patch to deal with lambdas introduced during search.
+    // lambdas can occur in terms both internalized and in raw form.
+    if (!found_complement && !is_or(f1) && num_proofs == 2) {
+        args.push_back(proofs[0]);
+        args.push_back(proofs[1]);
+        args.push_back(mk_false());
+        found_complement = true;
+    }
+
     if (!found_complement) {
         args.append(num_proofs, (expr**)proofs);
         CTRACE("mk_unit_resolution_bug", !is_or(f1), tout << mk_ll_pp(f1, *this) << "\n";
                for (unsigned i = 1; i < num_proofs; ++i)
                    tout << mk_pp(proofs[i], *this) << "\n";
+               tout << "facts\n";
+               for (unsigned i = 0; i < num_proofs; ++i)
+                   tout << mk_pp(get_fact(proofs[i]), *this) << "\n";
                );
         SASSERT(is_or(f1));
         ptr_buffer<expr> new_lits;