mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-09-21 12:24:34 -07:00
parent 527c5191a6 e8f4dd76c2
commit 516dba52ce
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_conflict_resolution.cpp
View file

@ -948,7 +948,7 @@ namespace smt {
//
// So, the test "m_ctx.get_justification(l.var()) == js" is used to check
// if l was assigned before ~l.
if (m_ctx.is_marked(l.var()) && m_ctx.get_justification(l.var()) == js) {
if ((m_ctx.is_marked(l.var()) && m_ctx.get_justification(l.var()) == js) || (js.get_kind() == b_justification::AXIOM)) {
expr_ref l_expr(m_manager);
m_ctx.literal2expr(l, l_expr);
proof * pr = m_manager.mk_hypothesis(l_expr.get());
@ -1065,7 +1065,7 @@ namespace smt {
m_js2proof.reset();
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
for (; it != end; ++it)
for (; it != end; ++it)
m_ctx.set_mark((*it).var());
}
@ -1076,6 +1076,8 @@ namespace smt {
return true;
SASSERT(js.get_kind() != b_justification::BIN_CLAUSE);
CTRACE("visit_b_justification_bug", js.get_kind() == b_justification::AXIOM, tout << "l: " << l << "\n"; m_ctx.display(tout););
if (js.get_kind() == b_justification::AXIOM)
return true;
SASSERT(js.get_kind() != b_justification::AXIOM);
if (js.get_kind() == b_justification::CLAUSE) {
clause * cls = js.get_clause();