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

proviso for ignore int

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-24 00:48:57 -07:00
parent 5c7eaec566
commit a24b5a64e1
2 changed files with 3 additions and 1 deletions

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

@ -609,7 +609,7 @@ namespace arith {
else if (v != euf::null_theory_var) {
rational r = get_value(v);
TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled()));
SASSERT("integer variables should have integer values: " && (ctx.get_config().m_arith_ignore_int || !a.is_int(o) || r.is_int() || m.limit().is_canceled()));
if (a.is_int(o) && !r.is_int())
r = floor(r);
value = a.mk_numeral(r, o->get_sort());

2
src/sat/smt/euf_model.cpp
View file

@ -320,6 +320,8 @@ namespace euf {
void solver::validate_model(model& mdl) {
if (!m_unhandled_functions.empty())
return;
if (get_config().m_arith_ignore_int)
return;
for (auto* s : m_solvers)
if (s && s->has_unhandled())
return;