From bbaedbcccc61b36f53791b874eba2771ed3d2dca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 May 2020 10:34:59 -0700 Subject: [PATCH] fix #4224 --- src/smt/theory_diff_logic_def.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 6fba631de..1772c7f0b 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -936,7 +936,10 @@ model_value_proc * theory_diff_logic::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)); }