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 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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-17 09:00:16 -08:00
parent 6e1c246454
commit 66fc873613
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_setup.cpp
View file

@ -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"));