diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp
index 82d351113..031c5098e 100644
--- a/src/muz/transforms/dl_mk_array_blast.cpp
+++ b/src/muz/transforms/dl_mk_array_blast.cpp
@@ -126,6 +126,12 @@ namespace datalog {
         app* s;
         var* v;
 
+        // disable Ackerman reduction if head contains a non-variable or non-constant argument.
+        for (unsigned i = 0; i < to_app(head)->get_num_args(); ++i) {
+            expr* arg = to_app(head)->get_arg(i);            
+            if (!is_var(arg) && !m.is_value(arg)) return false;
+        }
+
         for (unsigned i = 0; i < conjs.size(); ++i) {
             expr* e = conjs[i].get();
             if (is_select_eq_var(e, s, v)) {
@@ -281,6 +287,7 @@ namespace datalog {
         m_rewriter(body);
         sub(head);
         m_rewriter(head);
+        TRACE("dl", tout << body << " => " << head << "\n";);
         change = ackermanize(r, body, head);
         if (!change) {
             rules.add_rule(&r);
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
index ea0e6c887..455b06d3d 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
@@ -394,10 +394,6 @@ namespace datalog {
         m_simp(a, simp1_res);
         (*m_rw)(simp1_res.get(), res);
 
-        /*if (simp1_res.get()!=res.get()) {
-            std::cout<<"pre norm:\n"<<mk_pp(simp1_res.get(),m)<<"post norm:\n"<<mk_pp(res.get(),m)<<"\n";
-        }*/
-
         m_simp(res.get(), res);
     }
 
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index c06f82c8b..e6e9e863c 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -206,7 +206,8 @@ namespace smt {
         numeral k     = ceil(get_value(v));
         rational _k   = k.to_rational();
         expr_ref bound(get_manager());
-        bound  = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(_k, true));
+        expr* e = get_enode(v)->get_owner();
+        bound  = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e)));
         TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";);
         context & ctx = get_context();
         ctx.internalize(bound, true);
@@ -371,7 +372,7 @@ namespace smt {
         
         ctx.mk_th_axiom(get_id(), l1, l2);
        
-        TRACE("theory_arith_int", 
+        TRACE("arith_int", 
               tout << "cut: (or " << mk_pp(p1, get_manager()) << " " << mk_pp(p2, get_manager()) << ")\n";
               );
 
@@ -1407,6 +1408,7 @@ namespace smt {
             if (m_params.m_arith_int_eq_branching && branch_infeasible_int_equality()) {
                 return FC_CONTINUE;
             }
+
             theory_var int_var = find_infeasible_int_base_var();
             if (int_var != null_theory_var) {
                 TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";);