diff --git a/src/tactic/ackr/ackr_bound_probe.cpp b/src/tactic/ackr/ackr_bound_probe.cpp
index 2a527ecb4..cca2d6a90 100644
--- a/src/tactic/ackr/ackr_bound_probe.cpp
+++ b/src/tactic/ackr/ackr_bound_probe.cpp
@@ -16,6 +16,7 @@
 --*/
 #include"ackr_helper.h"
 #include"ackr_bound_probe.h"
+#include"ast_smt2_pp.h"
 
 /** \brief
  * For each function f, calculate the number of its occurrences o_f and compute "o_f choose 2".
@@ -66,7 +67,13 @@ public:
         proc::fun2terms_map::iterator it = p.m_fun2terms.begin();
         proc::fun2terms_map::iterator end = p.m_fun2terms.end();
         unsigned total = 0;
-        for (; it != end; ++it) total += n_choose_2(it->m_value->size());
+        for (; it != end; ++it) {
+            const unsigned fsz = it->m_value->size();
+            const unsigned n2 = n_choose_2(fsz);
+            TRACE("ackr_bound_probe", tout << mk_ismt2_pp(it->m_key, g.m(), 0) << " #" << fsz << " n_choose_2=" << n2 << std::endl;);
+            total += n2;
+        }
+        TRACE("ackr_bound_probe", tout << "total=" << total << std::endl;);
         return result(total);
     }
 
diff --git a/src/tactic/ackr/lackr_model_constructor.cpp b/src/tactic/ackr/lackr_model_constructor.cpp
index 2a38a1a4e..f9eded93b 100644
--- a/src/tactic/ackr/lackr_model_constructor.cpp
+++ b/src/tactic/ackr/lackr_model_constructor.cpp
@@ -190,17 +190,7 @@ struct lackr_model_constructor::imp {
             return true;
         }
 
-        inline bool is_val(expr * e) {
-            if (!is_app(e)) return false;
-            return is_val(to_app(e));
-        }
-
-        inline bool is_val(app * a) {
-            const family_id fid = a->get_decl()->get_family_id();
-            const bool rv = fid != null_family_id && a->get_num_args() == 0;
-            SASSERT(rv == (m_bv_rw.is_numeral(a) || m_m.is_true(a) || m_m.is_false(a)));
-            return rv;
-        }
+        inline bool is_val(expr * e) { return m_m.is_value(e); }
 
         inline bool eval_cached(app * a, expr *& val) {
             if (is_val(a)) { val = a; return true; }
diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index a03744474..56d8b1c88 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -33,6 +33,8 @@ Notes:
 
 #define MEMLIMIT 300
 
+#define ACKRLIMIT 1000
+
 tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
 
     params_ref solve_eq_p;
@@ -69,7 +71,7 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
             //
             using_params(mk_simplify_tactic(m), hoist_p),
             mk_max_bv_sharing_tactic(m),
-            when(mk_lt(mk_ackr_bound_probe(), mk_const_probe(static_cast<double>(100))),  mk_ackermannize_tactic(m,p))
+            when(mk_lt(mk_ackr_bound_probe(), mk_const_probe(static_cast<double>(ACKRLIMIT))),  mk_ackermannize_tactic(m,p))
             );
 }