From 338dfa906907a34f54f2edc045d0210a83b78f41 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 5 Feb 2024 14:02:46 -0300
Subject: [PATCH] more

---
 proofs/alf/rules/drat/Drat.smt3 |  9 +++++++--
 src/prop/prop_proof_manager.cpp | 20 ++------------------
 2 files changed, 9 insertions(+), 20 deletions(-)

diff --git a/proofs/alf/rules/drat/Drat.smt3 b/proofs/alf/rules/drat/Drat.smt3
index cafebbe197c..d64bc907f4f 100644
--- a/proofs/alf/rules/drat/Drat.smt3
+++ b/proofs/alf/rules/drat/Drat.smt3
@@ -68,9 +68,14 @@
   :conclusion false
 )
 
+(declare-oracle-fun run_sat_lemmas_prove (String Bool) Bool ./sat-lemmas-prove.sh)
 
-
-
+(declare-rule sat_lemmas_external_prove ((F Bool) (D String) (L Bool))
+  :premise-list F and
+  :args (D L)
+  :requires (((run_sat_lemmas_prove D L) true))
+  :conclusion false
+)
 
 ; run_sat_prove_dimacs takes:
 ; - A string corresponding to a DIMACS input.
diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp
index 74c4faebd06..4135eb01987 100644
--- a/src/prop/prop_proof_manager.cpp
+++ b/src/prop/prop_proof_manager.cpp
@@ -325,24 +325,8 @@ std::shared_ptr<ProofNode> PropPfManager::getProof(
     std::fstream dout(dinputFile.str(), std::ios::out);
     d_proofCnfStream->dumpDimacs(dout, inputs, lemmas);
     dout.close();
-
-    // Build the equalities between the lemma ids and the lemmas. Note that we
-    // expect that the order in which the ids are assigned to lemma clauses is
-    // the same as the one in which they are converted to DIMACs.
-    std::vector<Node> namedLemmas;
-    for (size_t i = 0, size = lemmas.size(); i < size; ++i)
-    {
-      std::stringstream lemmaId;
-      lemmaId << "@l" << i;
-      Node lemmaIdNode = nm->mkRawSymbol(lemmaId.str(), bt);
-      namedLemmas.push_back(nm->mkNode(Kind::SEXPR,
-                                       {nm->mkRawSymbol("!", bt),
-                                        lemmas[i],
-                                        nm->mkRawSymbol(":named", bt),
-                                        lemmaIdNode}));
-    }
-    args.push_back(lemmas.size() > 1 ? nm->mkNode(Kind::AND, namedLemmas)
-                                     : namedLemmas[0]);
+    args.push_back(lemmas.size() > 1 ? nm->mkNode(Kind::AND, lemmas)
+                                     : lemmas[0]);
     // build the proof node
     CDProof cdp(d_env);
     Node falseNode = nm->mkConst(false);