mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

create proof object in elim01. Codeplex issue 158

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-01-03 11:04:08 -08:00
parent 2cd4669e21
commit 2f9e9e1a3c
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/tactic/arith/elim01_tactic.cpp
View file

@ -193,11 +193,14 @@ public:
expr_ref new_curr(m), tmp_curr(m); expr_ref new_curr(m), tmp_curr(m);
proof_ref new_pr(m); proof_ref new_pr(m);
for (unsigned i = 0; i < g->size(); i++) { for (unsigned i = 0; i < g->size(); i++) {
expr * curr = g->form(i); expr * curr = g->form(i);
sub(curr, tmp_curr); sub(curr, tmp_curr);
m_rewriter(tmp_curr, new_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)); g->update(i, new_curr, new_pr, g->dep(i));
} }
for (unsigned i = 0; i < axioms.size(); ++i) { for (unsigned i = 0; i < axioms.size(); ++i) {