From 66fc873613a80c5f2935fbeb29ced4ae8ec2b405 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Nov 2015 09:00:16 -0800 Subject: [PATCH] Fix for #322: PDR engine cannot falls back on fixed size arithmetic for difference logic. It would eventually overflow and cause incorrect model construction. Enable only fixed-size arithmetic when configuration allows it Signed-off-by: Nikolaj Bjorner --- src/smt/smt_setup.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 524dbeab6..edb4f1e55 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -721,8 +721,8 @@ namespace smt { IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";); st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas()); IF_VERBOSE(1000, st.display_primitive(verbose_stream());); - bool fixnum = st.arith_k_sum_is_small(); - bool int_only = !st.m_has_rational && !st.m_has_real; + bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum; + bool int_only = !st.m_has_rational && !st.m_has_real && m_params.m_arith_int_only; switch(m_params.m_arith_mode) { case AS_NO_ARITH: m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));