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

fix #4224

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-06 10:34:59 -07:00
parent 6f6c8d76eb
commit bbaedbcccc
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_diff_logic_def.h
View file

@ -936,7 +936,10 @@ model_value_proc * theory_diff_logic<Ext>::mk_value(enode * n, model_generator &
num = val.get_rational().to_rational() + m_delta * val.get_infinitesimal().to_rational();
}
TRACE("arith", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";);
return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, m_util.is_int(n->get_owner())));
bool is_int = m_util.is_int(n->get_owner());
if (is_int && !num.is_int())
throw default_exception("difference logic solver was used on mixed int/real problem");
return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, is_int));
}