diff --git a/src/tactic/ackr/ackermannize_tactic.cpp b/src/tactic/ackr/ackermannize_tactic.cpp
index 6e95d564b..1345b9415 100644
--- a/src/tactic/ackr/ackermannize_tactic.cpp
+++ b/src/tactic/ackr/ackermannize_tactic.cpp
@@ -35,6 +35,10 @@ public:
         expr_dependency_ref & core) {
         mc = 0;
         ast_manager& m(g->m());
+		tactic_report report("ackermannize", *g);
+		fail_if_unsat_core_generation("ackermannize", g);
+		fail_if_proof_generation("ackermannize", g);
+				
         expr_ref_vector flas(m);
         const unsigned sz = g->size();
         for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
@@ -48,6 +52,10 @@ public:
         if (g->models_enabled()) {
             mc = mk_ackr_model_converter(m, imp->get_info());
         }
+
+		resg->inc_depth();
+		TRACE("ackermannize", resg->display(tout););
+		SASSERT(resg->is_well_sorted());
     }
 
     virtual void collect_statistics(statistics & st) const {
diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp
index bb9a8fb32..a12d2c90d 100644
--- a/src/tactic/probe.cpp
+++ b/src/tactic/probe.cpp
@@ -285,9 +285,16 @@ struct is_non_qfbv_predicate {
             throw found();
         family_id fid = n->get_family_id();
         if (fid == m.get_basic_family_id()) 
-            return; 
-        if (fid == u.get_family_id())
-            return;
+            return;				
+        if (fid == u.get_family_id()) {
+			if (n->get_decl_kind() == OP_BSDIV0 ||
+				n->get_decl_kind() == OP_BUDIV0 ||
+				n->get_decl_kind() == OP_BSREM0 ||
+				n->get_decl_kind() == OP_BUREM0 ||
+				n->get_decl_kind() == OP_BSMOD0)				
+				throw found();
+			return;
+		}
         if (is_uninterp_const(n))
             return;
         throw found();
@@ -305,8 +312,6 @@ public:
 class is_qfbv_probe : public probe {
 public:
     virtual result operator()(goal const & g) {
-        bv_rewriter rw(g.m());
-        if (!rw.hi_div0()) return false;
         return !test<is_non_qfbv_predicate>(g);
     }
 };