mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

fix #3634

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 20:33:42 -07:00
parent 79183b6339
commit fe267803d1
3 changed files with 19 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/smt/smt_context.cpp
View file

@ -2950,7 +2950,7 @@ namespace smt {
void context::assert_expr_core(expr * e, proof * pr) { void context::assert_expr_core(expr * e, proof * pr) {
if (get_cancel_flag()) return; if (get_cancel_flag()) return;
SASSERT(is_well_sorted(m, e)); SASSERT(is_well_sorted(m, e));
TRACE("begin_assert_expr", tout << this << " " << mk_pp(e, m) << "\n";); TRACE("begin_assert_expr", tout << mk_pp(e, m) << " " << mk_pp(pr, m) << "\n";);
TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m) << "\n";); TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m) << "\n";);
pop_to_base_lvl(); pop_to_base_lvl();
if (pr == nullptr) if (pr == nullptr)
@ -3141,20 +3141,24 @@ namespace smt {
m_asserted_formulas.commit(); m_asserted_formulas.commit();
} }
if (m_asserted_formulas.inconsistent() && !inconsistent()) { if (m_asserted_formulas.inconsistent() && !inconsistent()) {
proof * pr = m_asserted_formulas.get_inconsistency_proof(); asserted_inconsistent();
if (pr == nullptr) {
set_conflict(b_justification::mk_axiom());
}
else {
set_conflict(mk_justification(justification_proof_wrapper(*this, pr)));
m_unsat_proof = pr;
}
} }
TRACE("internalize_assertions", tout << "after internalize_assertions()...\n"; TRACE("internalize_assertions", tout << "after internalize_assertions()...\n";
tout << "inconsistent: " << inconsistent() << "\n";); tout << "inconsistent: " << inconsistent() << "\n";);
TRACE("after_internalize_assertions", display(tout);); TRACE("after_internalize_assertions", display(tout););
} }
void context::asserted_inconsistent() {
proof * pr = m_asserted_formulas.get_inconsistency_proof();
m_unsat_proof = pr;
if (!pr) {
set_conflict(b_justification::mk_axiom());
}
else {
set_conflict(mk_justification(justification_proof_wrapper(*this, pr)));
}
}
/** /**
\brief Assumptions must be uninterpreted boolean constants (aka propositional variables). \brief Assumptions must be uninterpreted boolean constants (aka propositional variables).
*/ */
@ -3626,8 +3630,10 @@ namespace smt {
lbool context::search() { lbool context::search() {
if (m_asserted_formulas.inconsistent()) if (m_asserted_formulas.inconsistent()) {
asserted_inconsistent();
return l_false; return l_false;
}
if (inconsistent()) { if (inconsistent()) {
VERIFY(!resolve_conflict()); VERIFY(!resolve_conflict());
return l_false; return l_false;

2
src/smt/smt_context.h
View file

@ -1138,6 +1138,8 @@ namespace smt {
void internalize_assertions(); void internalize_assertions();
void asserted_inconsistent();
bool validate_assumptions(expr_ref_vector const& asms); bool validate_assumptions(expr_ref_vector const& asms);
void init_assumptions(expr_ref_vector const& asms); void init_assumptions(expr_ref_vector const& asms);

1
src/smt/tactic/smt_tactic.cpp
View file

@ -249,6 +249,7 @@ public:
lcore = m.mk_join(lcore, m.mk_leaf(d)); lcore = m.mk_join(lcore, m.mk_leaf(d));
} }
} }
if (!pr && m.proofs_enabled()) pr = m.mk_asserted(m.mk_false()); // bail out
in->assert_expr(m.mk_false(), pr, lcore); in->assert_expr(m.mk_false(), pr, lcore);
result.push_back(in.get()); result.push_back(in.get());
return; return;