mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
debugging assertion violation
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
dffb0ff844
commit
fe6af38d97
|
@ -78,7 +78,7 @@ struct mus::imp {
|
|||
expr_ref_vector assumptions(m);
|
||||
ptr_vector<expr> core_exprs;
|
||||
while (!core.empty()) {
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";);
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";);
|
||||
unsigned cls_id = core.back();
|
||||
TRACE("opt",
|
||||
display_vec(tout << "core: ", core);
|
||||
|
|
|
@ -72,6 +72,7 @@ namespace smt {
|
|||
m_value .push_back(inf_numeral());
|
||||
}
|
||||
m_old_value .push_back(inf_numeral());
|
||||
SASSERT(m_var_occs.size() == r);
|
||||
m_var_occs .push_back(atoms());
|
||||
m_unassigned_atoms .push_back(0);
|
||||
m_var_pos .push_back(-1);
|
||||
|
@ -85,6 +86,7 @@ namespace smt {
|
|||
if (is_pure_monomial(n->get_owner()))
|
||||
m_nl_monomials.push_back(r);
|
||||
SASSERT(check_vector_sizes());
|
||||
SASSERT(m_var_occs[r].empty());
|
||||
TRACE("mk_arith_var",
|
||||
tout << "#" << n->get_owner_id() << " :=\n" << mk_ll_pp(n->get_owner(), get_manager()) << "\n";
|
||||
tout << "is_attached_to_var: " << is_attached_to_var(n) << ", var: " << n->get_th_var(get_id()) << "\n";);
|
||||
|
@ -812,6 +814,7 @@ namespace smt {
|
|||
void theory_arith<Ext>::mk_bound_axioms(atom * a1) {
|
||||
theory_var v = a1->get_var();
|
||||
atoms & occs = m_var_occs[v];
|
||||
TRACE("mk_bound_axioms", tout << "add bound axioms for v" << v << " " << a1 << "\n";);
|
||||
if (!get_context().is_searching()) {
|
||||
//
|
||||
// NB. We make an assumption that user push calls propagation
|
||||
|
@ -823,7 +826,7 @@ namespace smt {
|
|||
}
|
||||
inf_numeral const & k1(a1->get_k());
|
||||
atom_kind kind1 = a1->get_atom_kind();
|
||||
TRACE("mk_bound_axioms", tout << "making bound axioms for v" << v << " " << kind1 << " " << k1 << "\n";);
|
||||
TRACE("mk_bound_axioms", tout << "making bound axioms for v" << v << " " << kind1 << " " << k1 << " " << a1 << "\n";);
|
||||
typename atoms::iterator it = occs.begin();
|
||||
typename atoms::iterator end = occs.end();
|
||||
|
||||
|
@ -833,6 +836,12 @@ namespace smt {
|
|||
atom * a2 = *it;
|
||||
inf_numeral const & k2(a2->get_k());
|
||||
atom_kind kind2 = a2->get_atom_kind();
|
||||
CTRACE("mk_bound_axioms", k1 == k2 && kind1 == kind2,
|
||||
display_atom(tout << a1 << " ", a1, true);
|
||||
display_atom(tout << a2 << " ", a2, true);
|
||||
tout << &occs << " " << &m_var_occs[v] << "\n";
|
||||
);
|
||||
|
||||
SASSERT(k1 != k2 || kind1 != kind2);
|
||||
if (kind2 == A_LOWER) {
|
||||
if (k2 < k1) {
|
||||
|
@ -861,6 +870,7 @@ namespace smt {
|
|||
|
||||
template<typename Ext>
|
||||
void theory_arith<Ext>::mk_bound_axiom(atom* a1, atom* a2) {
|
||||
TRACE("mk_bound_axioms", tout << a1 << " " << a2 << "\n";);
|
||||
theory_var v = a1->get_var();
|
||||
literal l1(a1->get_bool_var());
|
||||
literal l2(a2->get_bool_var());
|
||||
|
@ -1090,7 +1100,8 @@ namespace smt {
|
|||
occs.push_back(a);
|
||||
m_atoms.push_back(a);
|
||||
insert_bv2a(bv, a);
|
||||
TRACE("arith_internalize", tout << "succeeded... v: " << v << " " << kind << " " << k << "\n";);
|
||||
TRACE("arith_internalize", tout << "succeeded... v" << v << " " << kind << " " << k << "\n";
|
||||
for (unsigned i = 0; i + 1 < occs.size(); ++i) tout << occs[i] << "\n";);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -2062,7 +2073,7 @@ namespace smt {
|
|||
continue;
|
||||
SASSERT(curr_error > inf_numeral(0));
|
||||
if (best == null_theory_var || (!least && curr_error > best_error) || (least && curr_error < best_error)) {
|
||||
TRACE("select_pivot", tout << "best: " << best << " v: " << v
|
||||
TRACE("select_pivot", tout << "best: " << best << " v" << v
|
||||
<< ", best_error: " << best_error << ", curr_error: " << curr_error << "\n";);
|
||||
best = v;
|
||||
best_error = curr_error;
|
||||
|
@ -2619,9 +2630,9 @@ namespace smt {
|
|||
<< limit_k1 << " delta: " << delta << " coeff: " << coeff << "\n";);
|
||||
inf_numeral k_2 = k_1;
|
||||
atom * new_atom = 0;
|
||||
atoms & as = m_var_occs[it->m_var];
|
||||
typename atoms::iterator it = as.begin();
|
||||
typename atoms::iterator end = as.end();
|
||||
atoms const & as = m_var_occs[it->m_var];
|
||||
typename atoms::const_iterator it = as.begin();
|
||||
typename atoms::const_iterator end = as.end();
|
||||
for (; it != end; ++it) {
|
||||
atom * a = *it;
|
||||
if (a == b)
|
||||
|
@ -3200,6 +3211,7 @@ namespace smt {
|
|||
erase_bv2a(bv);
|
||||
SASSERT(m_var_occs[v].back() == a);
|
||||
m_var_occs[v].pop_back();
|
||||
TRACE("mk_bound_axioms", tout << a << "\n";);
|
||||
dealloc(a);
|
||||
}
|
||||
m_atoms.shrink(old_size);
|
||||
|
@ -3269,6 +3281,7 @@ namespace smt {
|
|||
m_bounds[1] .shrink(old_num_vars);
|
||||
SASSERT(check_vector_sizes());
|
||||
}
|
||||
SASSERT(m_var_occs.size() == old_num_vars);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
|
|
Loading…
Reference in a new issue