mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

fix crash in proof generation in BMC

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-05-29 17:56:23 -07:00
parent 9a66696639
commit 60c4973c1d
1 changed files with 23 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/muz_qe/dl_bmc_engine.cpp
View file

@ -297,6 +297,7 @@ namespace datalog {
r->to_formula(fml); r->to_formula(fml);
r2 = r; r2 = r;
rm.substitute(r2, sub.size(), sub.c_ptr()); rm.substitute(r2, sub.size(), sub.c_ptr());
proof_ref p(m);
if (r0) { if (r0) {
VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get()));
expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true);
@ -306,7 +307,10 @@ namespace datalog {
r1->to_formula(concl); r1->to_formula(concl);
scoped_proof _sp(m); scoped_proof _sp(m);
proof* p = r->get_proof(); p = r->get_proof();
if (!p) {
p = m.mk_asserted(fml);
}
proof* premises[2] = { pr, p }; proof* premises[2] = { pr, p };
positions.push_back(std::make_pair(0, 1)); positions.push_back(std::make_pair(0, 1));
@ -319,13 +323,17 @@ namespace datalog {
else { else {
r2->to_formula(concl); r2->to_formula(concl);
scoped_proof _sp(m); scoped_proof _sp(m);
proof* p = r->get_proof(); p = r->get_proof();
if (!p) {
p = m.mk_asserted(fml);
}
if (sub.empty()) { if (sub.empty()) {
pr = p; pr = p;
} }
else { else {
substs.push_back(sub); substs.push_back(sub);
pr = m.mk_hyper_resolve(1, &p, concl, positions, substs); proof* ps[1] = { p };
pr = m.mk_hyper_resolve(1, ps, concl, positions, substs);
} }
r0 = r2; r0 = r2;
} }
@ -1211,6 +1219,15 @@ namespace datalog {
r->to_formula(fml); r->to_formula(fml);
r2 = r; r2 = r;
rm.substitute(r2, sub.size(), sub.c_ptr()); rm.substitute(r2, sub.size(), sub.c_ptr());
proof_ref p(m);
{
scoped_proof _sp(m);
p = r->get_proof();
if (!p) {
p = m.mk_asserted(fml);
}
}
if (r0) { if (r0) {
VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get()));
expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true);
@ -1218,9 +1235,8 @@ namespace datalog {
apply_subst(sub, sub2); apply_subst(sub, sub2);
unifier.apply(*r0.get(), 0, *r2.get(), r1); unifier.apply(*r0.get(), 0, *r2.get(), r1);
r1->to_formula(concl); r1->to_formula(concl);
scoped_proof _sp(m);
proof* p = r->get_proof(); scoped_proof _sp(m);
proof* premises[2] = { pr, p }; proof* premises[2] = { pr, p };
positions.push_back(std::make_pair(0, 1)); positions.push_back(std::make_pair(0, 1));
@ -1233,13 +1249,13 @@ namespace datalog {
else { else {
r2->to_formula(concl); r2->to_formula(concl);
scoped_proof _sp(m); scoped_proof _sp(m);
proof* p = r->get_proof();
if (sub.empty()) { if (sub.empty()) {
pr = p; pr = p;
} }
else { else {
substs.push_back(sub); substs.push_back(sub);
pr = m.mk_hyper_resolve(1, &p, concl, positions, substs); proof * ps[1] = { p };
pr = m.mk_hyper_resolve(1, ps, concl, positions, substs);
} }
r0 = r2; r0 = r2;
} }