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

fix #4107

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-26 13:45:29 -07:00
parent 16d34b9fcc
commit d3094291d3
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_diff_logic_def.h
View file

@ -923,8 +923,11 @@ template<typename Ext>
model_value_proc * theory_diff_logic<Ext>::mk_value(enode * n, model_generator & mg) { model_value_proc * theory_diff_logic<Ext>::mk_value(enode * n, model_generator & mg) {
theory_var v = n->get_th_var(get_id()); theory_var v = n->get_th_var(get_id());
SASSERT(v != null_theory_var); SASSERT(v != null_theory_var);
numeral val = m_graph.get_assignment(v); rational num;
rational num = val.get_rational().to_rational() + m_delta * val.get_infinitesimal().to_rational(); if (!m_util.is_numeral(n->get_owner(), num)) {
numeral val = m_graph.get_assignment(v);
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";); 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()))); return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, m_util.is_int(n->get_owner())));
} }