mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix regressions exposed in QF_LIA: manager got initialized early and Euclidean solver is not safe even with some throttle

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-23 20:38:18 -07:00
parent 87989dd93e
commit fe4f3e7772
2 changed files with 10 additions and 8 deletions

16
src/opt/opt_cmds.cpp
View file

@ -138,18 +138,18 @@ public:
};
class alternate_min_max_cmd : public cmd {
app_ref_vector m_vars;
app_ref_vector* m_vars;
svector<bool> m_is_max;
unsigned m_position;
public:
alternate_min_max_cmd(ast_manager& m):
alternate_min_max_cmd():
cmd("min-max"),
m_vars(m),
m_vars(0),
m_position(0)
{}
virtual void reset(cmd_context & ctx) {
m_vars.reset();
dealloc(m_vars);
m_is_max.reset();
m_position = 0;
}
@ -176,7 +176,8 @@ public:
}
else {
m_is_max.push_back(is_max);
m_vars.push_back(ctx.m().mk_const(ctx.find_func_decl(slist[i])));
if (!m_vars) m_vars = alloc(app_ref_vector, ctx.m());
m_vars->push_back(ctx.m().mk_const(ctx.find_func_decl(slist[i])));
}
}
++m_position;
@ -187,7 +188,8 @@ public:
throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable");
}
++m_position;
get_opt(ctx).min_max(to_app(t), m_vars, m_is_max);
if (!m_vars) m_vars = alloc(app_ref_vector, ctx.m());
get_opt(ctx).min_max(to_app(t), *m_vars, m_is_max);
}
virtual void failure_cleanup(cmd_context & ctx) {
@ -202,7 +204,7 @@ void install_opt_cmds(cmd_context & ctx) {
ctx.insert(alloc(assert_soft_cmd));
ctx.insert(alloc(min_maximize_cmd, true));
ctx.insert(alloc(min_maximize_cmd, false));
ctx.insert(alloc(alternate_min_max_cmd, ctx.m()));
ctx.insert(alloc(alternate_min_max_cmd));
}

2
src/smt/theory_arith_int.h
View file

@ -1308,7 +1308,7 @@ namespace smt {
if (!gcd_test())
return FC_CONTINUE;
if (m_params.m_arith_euclidean_solver || (0 == (1 + m_branch_cut_counter) % 80))
if (m_params.m_arith_euclidean_solver)
apply_euclidean_solver();
if (get_context().inconsistent())