mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 04:15:51 +00:00
Code Activity

fix crash reported in #946

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-16 18:56:43 -07:00
parent 72651e2e98
commit a0237ed2a6
2 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/opt/opt_solver.cpp
View file

@ -50,6 +50,7 @@ namespace opt {
if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
m_params.m_relevancy_lvl = 0;
}
// m_params.m_auto_config = false;
}
unsigned opt_solver::m_dump_count = 0;

9
src/smt/theory_dense_diff_logic_def.h
View file

@ -901,7 +901,7 @@ namespace smt {
objective_term const& objective = m_objectives[v];
has_shared = false;
IF_VERBOSE(1,
IF_VERBOSE(4,
for (unsigned i = 0; i < objective.size(); ++i) {
verbose_stream() << objective[i].second
<< " * v" << objective[i].first << " ";
@ -991,9 +991,12 @@ namespace smt {
if (num_nodes <= v && v < num_nodes + num_edges) {
unsigned edge_id = v - num_nodes;
literal lit = m_edges[edge_id].m_justification;
get_context().literal2expr(lit, tmp);
core.push_back(tmp);
if (lit != null_literal) {
get_context().literal2expr(lit, tmp);
core.push_back(tmp);
}
}
TRACE("opt", tout << core << "\n";);
}
for (unsigned i = 0; i < num_nodes; ++i) {
mpq_inf const& val = S.get_value(i);