From 2f9e9e1a3c2aaf514e69d1bd944e22ce3fc3b264 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Jan 2015 11:04:08 -0800 Subject: [PATCH] create proof object in elim01. Codeplex issue 158 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/elim01_tactic.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp index 53fa948ce..dda3d8fc9 100644 --- a/src/tactic/arith/elim01_tactic.cpp +++ b/src/tactic/arith/elim01_tactic.cpp @@ -193,11 +193,14 @@ public: expr_ref new_curr(m), tmp_curr(m); proof_ref new_pr(m); - for (unsigned i = 0; i < g->size(); i++) { expr * curr = g->form(i); sub(curr, tmp_curr); m_rewriter(tmp_curr, new_curr); + if (m.proofs_enabled()) { + new_pr = m.mk_rewrite(curr, new_curr); + new_pr = m.mk_modus_ponens(g->pr(i), new_pr); + } g->update(i, new_curr, new_pr, g->dep(i)); } for (unsigned i = 0; i < axioms.size(); ++i) {