mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #2107

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-27 19:45:19 -08:00
parent 94dae2da3a
commit 4f988595c7
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_context.cpp
View file

@ -3244,8 +3244,13 @@ namespace smt {
proof * pr = m_manager.mk_asserted(curr_assumption); proof * pr = m_manager.mk_asserted(curr_assumption);
internalize_assertion(curr_assumption, pr, 0); internalize_assertion(curr_assumption, pr, 0);
literal l = get_literal(curr_assumption); literal l = get_literal(curr_assumption);
if (l == true_literal)
continue;
if (l == false_literal) {
set_conflict(b_justification::mk_axiom());
break;
}
m_literal2assumption.insert(l.index(), orig_assumption); m_literal2assumption.insert(l.index(), orig_assumption);
// mark_as_relevant(l); <<< not needed
// internalize_assertion marked l as relevant. // internalize_assertion marked l as relevant.
SASSERT(is_relevant(l)); SASSERT(is_relevant(l));
TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m_manager) << "\n";); TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m_manager) << "\n";);