mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fix seg-fault from #1244
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
799fb4a0d1
commit
a4cf2726fd
|
@ -1946,7 +1946,7 @@ bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr*
|
|||
}
|
||||
}
|
||||
|
||||
if (szr == 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) {
|
||||
if (szr == 1 && szl >= 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) {
|
||||
return solve_itos(szr, rs, szl, ls, rhs, lhs, is_sat);
|
||||
}
|
||||
|
||||
|
|
|
@ -96,6 +96,8 @@ class asserted_formulas {
|
|||
void max_bv_sharing();
|
||||
bool canceled() { return m.canceled(); }
|
||||
|
||||
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
|
||||
|
||||
public:
|
||||
asserted_formulas(ast_manager & m, smt_params & p);
|
||||
~asserted_formulas();
|
||||
|
@ -118,7 +120,6 @@ public:
|
|||
proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
|
||||
expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); }
|
||||
proof * const * get_formula_proofs() const { return m_asserted_formula_prs.c_ptr(); }
|
||||
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
|
||||
void register_simplifier_plugin(simplifier_plugin * p) { m_simplifier.register_plugin(p); }
|
||||
simplifier & get_simplifier() { return m_simplifier; }
|
||||
void get_assertions(ptr_vector<expr> & result);
|
||||
|
|
|
@ -348,10 +348,8 @@ namespace smt {
|
|||
literal_vector & antecedents = m_tmp_literal_vector;
|
||||
antecedents.reset();
|
||||
justification2literals_core(js, antecedents);
|
||||
literal_vector::iterator it = antecedents.begin();
|
||||
literal_vector::iterator end = antecedents.end();
|
||||
for(; it != end; ++it)
|
||||
process_antecedent(*it, num_marks);
|
||||
for (literal l : antecedents)
|
||||
process_antecedent(l, num_marks);
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -517,11 +515,13 @@ namespace smt {
|
|||
}
|
||||
|
||||
TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
|
||||
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";);
|
||||
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n";
|
||||
);
|
||||
SASSERT(js != null_b_justification);
|
||||
switch (js.get_kind()) {
|
||||
case b_justification::CLAUSE: {
|
||||
clause * cls = js.get_clause();
|
||||
TRACE("conflict", m_ctx.display_clause_detail(tout, cls););
|
||||
if (cls->is_lemma())
|
||||
cls->inc_clause_activity();
|
||||
unsigned num_lits = cls->get_num_literals();
|
||||
|
@ -566,7 +566,7 @@ namespace smt {
|
|||
if (m_ctx.is_marked(l.var()))
|
||||
break;
|
||||
CTRACE("conflict", m_ctx.get_assign_level(l) != m_conflict_lvl && m_ctx.get_assign_level(l) != m_ctx.get_base_level(),
|
||||
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal(tout, l);
|
||||
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal_verbose(tout, l);
|
||||
tout << "\n";);
|
||||
SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl ||
|
||||
// it may also be an (out-of-order) asserted literal
|
||||
|
|
Loading…
Reference in a new issue