From 56bfc06c4f7e33d4249551e269e443b19f71ef89 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 2 Jun 2013 20:55:15 -0700
Subject: [PATCH] fix reference count bugs in overflow/underflow APIs for
 bit-vectors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz_qe/qe.cpp                      | 2 +-
 src/smt/params/theory_arith_params.cpp | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp
index 5603b8102..894a935b5 100644
--- a/src/muz_qe/qe.cpp
+++ b/src/muz_qe/qe.cpp
@@ -2084,7 +2084,7 @@ namespace qe {
             
             flet<bool> fl1(m_fparams.m_model, true);
             flet<bool> fl2(m_fparams.m_simplify_bit2int, true);
-            //flet<bool> fl3(m_fparams.m_arith_enum_const_mod, true);
+            flet<bool> fl3(m_fparams.m_arith_enum_const_mod, true);
             flet<bool> fl4(m_fparams.m_bv_enable_int2bv2int, true);
             flet<bool> fl5(m_fparams.m_array_canonize_simplify, true);
             flet<unsigned> fl6(m_fparams.m_relevancy_lvl, 0);
diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp
index dcffa83dc..7281a5daa 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/smt/params/theory_arith_params.cpp
@@ -33,7 +33,6 @@ void theory_arith_params::updt_params(params_ref const & _p) {
     m_arith_int_eq_branching = p.arith_int_eq_branch();
     m_arith_ignore_int = p.arith_ignore_int();
     m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
-    m_arith_enum_const_mod = true;
 }