mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

enable new core for incremental mode

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-01-11 14:55:17 -08:00
parent 2ead209d40
commit 0e429cab33
2 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/arith_axioms.cpp
View file

@ -405,9 +405,13 @@ namespace arith {
expr* n = m_idiv_terms[i];
expr* p = nullptr, * q = nullptr;
VERIFY(a.is_idiv(n, p, q));
theory_var v = mk_evar(n);
euf::enode* np = ctx.get_enode(p);
euf::enode* nn = ctx.get_enode(n);
if (!np || !np->is_attached_to(get_id()))
continue;
if (!nn || !nn->is_attached_to(get_id()))
continue;
theory_var v1 = mk_evar(p);
if (!is_registered_var(v1))
continue;
lp::impq r1 = get_ivalue(v1);
@ -428,6 +432,7 @@ namespace arith {
TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";);
continue;
}
theory_var v = mk_evar(n);
if (!is_registered_var(v))
continue;
lp::impq val_v = get_ivalue(v);

3
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -116,8 +116,11 @@ static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p
static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
bv_rewriter rw(m);
solver* s = mk_special_solver_for_logic(m, p, logic);
tactic_params tp;
if (!s && logic == "QF_BV" && rw.hi_div0())
s = mk_inc_sat_solver(m, p);
if (!s && tp.default_tactic() == "sat")
s = mk_inc_sat_solver(m, p);
if (!s)
s = mk_smt_solver(m, p, logic);
return s;