mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

#5223

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-05 16:57:06 -07:00
parent 87c0a8136f
commit 7e330c15e7
2 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -580,6 +580,7 @@ namespace arith {
verbose_stream() << n->bool_var() << " " << n->value() << " " << get_phase(n->bool_var()) << " " << ctx.bpp(n) << "\n";
verbose_stream() << *b << "\n";);
IF_VERBOSE(0, ctx.display(verbose_stream()));
IF_VERBOSE(0, verbose_stream() << mdl << "\n");
UNREACHABLE();
}
}
@ -1438,4 +1439,12 @@ namespace arith {
ctx.get_antecedents(l, jst, r, probing);
}
bool solver::include_func_interp(func_decl* f) const {
return
a.is_div0(f) ||
a.is_idiv0(f) ||
a.is_power0(f) ||
a.is_rem0(f) ||
a.is_mod0(f);
}
}

1
src/sat/smt/arith_solver.h
View file

@ -444,6 +444,7 @@ namespace arith {
void apply_sort_cnstr(euf::enode* n, sort* s) override {}
bool is_shared(theory_var v) const override;
lbool get_phase(bool_var v) override;
bool include_func_interp(func_decl* f) const override;
// bounds and equality propagation callbacks
lp::lar_solver& lp() { return *m_solver; }