From 53b6059276342522c938b8652103fc093a988744 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Nov 2022 11:59:56 -0800 Subject: [PATCH] bypass built-in proof objects for clause trail the build-in proof constructors are not flexible when it comes to allowing alternation of justified lemmas and lemmas without justifications. --- src/smt/smt_clause_proof.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp index a2bc381e4..ad3d3818c 100644 --- a/src/smt/smt_clause_proof.cpp +++ b/src/smt/smt_clause_proof.cpp @@ -147,18 +147,22 @@ namespace smt { for (auto& info : m_trail) { expr_ref fact = mk_or(info.m_clause); proof* pr = info.m_proof; + expr* args[2] = { pr, fact }; + unsigned num_args = 2, offset = 0; + if (!pr) + offset = 1; switch (info.m_status) { case status::assumption: - ps.push_back(m.mk_assumption_add(pr, fact)); + ps.push_back(m.mk_app(symbol("assumption"), num_args - offset, args + offset, m.mk_proof_sort())); break; case status::lemma: - ps.push_back(m.mk_lemma_add(pr, fact)); + ps.push_back(m.mk_app(symbol("lemma"), num_args - offset, args + offset, m.mk_proof_sort())); break; case status::th_assumption: - ps.push_back(m.mk_th_assumption_add(pr, fact)); + ps.push_back(m.mk_app(symbol("th-assumption"), num_args - offset, args + offset, m.mk_proof_sort())); break; case status::th_lemma: - ps.push_back(m.mk_th_lemma_add(pr, fact)); + ps.push_back(m.mk_app(symbol("th-lemma"), num_args - offset, args + offset, m.mk_proof_sort())); break; case status::deleted: ps.push_back(m.mk_redundant_del(fact));