mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

fix #1538

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-17 11:25:07 -07:00
parent aa913c564c
commit 72f8e408fc
2 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_context_pp.cpp
View file

@ -580,20 +580,20 @@ namespace smt {
case b_justification::BIN_CLAUSE: { case b_justification::BIN_CLAUSE: {
literal l2 = j.get_literal(); literal l2 = j.get_literal();
out << "bin-clause "; out << "bin-clause ";
display_literal(out, l2); display_literal_verbose(out, l2);
break; break;
} }
case b_justification::CLAUSE: { case b_justification::CLAUSE: {
clause * cls = j.get_clause(); clause * cls = j.get_clause();
out << "clause "; out << "clause ";
if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals()); if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals());
break; break;
} }
case b_justification::JUSTIFICATION: { case b_justification::JUSTIFICATION: {
out << "justification " << j.get_justification()->get_from_theory() << ": "; out << "justification " << j.get_justification()->get_from_theory() << ": ";
literal_vector lits; literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits); const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
display_literals(out, lits); display_literals_verbose(out, lits);
break; break;
} }
default: default:

8
src/smt/theory_seq.cpp
View file

@ -2404,8 +2404,7 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
lits.push_back(~is_digit(ith_char)); lits.push_back(~is_digit(ith_char));
nums.push_back(digit2int(ith_char)); nums.push_back(digit2int(ith_char));
} }
for (unsigned i = sz-1, c = 1; i > 0; c *= 10) { for (unsigned i = sz, c = 1; i-- > 0; c *= 10) {
--i;
coeff = m_autil.mk_int(c); coeff = m_autil.mk_int(c);
nums[i] = m_autil.mk_mul(coeff, nums[i].get()); nums[i] = m_autil.mk_mul(coeff, nums[i].get());
} }
@ -2414,9 +2413,10 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
lits.push_back(mk_eq(e, num, false)); lits.push_back(mk_eq(e, num, false));
++m_stats.m_add_axiom; ++m_stats.m_add_axiom;
m_new_propagation = true; m_new_propagation = true;
for (unsigned i = 0; i < lits.size(); ++i) { for (literal lit : lits) {
ctx.mark_as_relevant(lits[i]); ctx.mark_as_relevant(lit);
} }
TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
m_stoi_axioms.insert(val); m_stoi_axioms.insert(val);
m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_stoi_axioms, val)); m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_stoi_axioms, val));