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

#6523

Browse source 
malformed models on giveup status
This commit is contained in:
Nikolaj Bjorner 2023-11-13 14:32:53 -08:00
parent 8a4e857294
commit c2610cb37c
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -632,7 +632,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: " && (ctx.get_config().m_arith_ignore_int || !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_not_handled != nullptr || m.limit().is_canceled()));
if (a.is_int(o) && !r.is_int())
r = floor(r);
value = a.mk_numeral(r, o->get_sort());