diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp
index 35cb5891f..e43adee02 100644
--- a/src/ast/macros/macro_finder.cpp
+++ b/src/ast/macros/macro_finder.cpp
@@ -22,13 +22,13 @@ Revision History:
 #include"ast_pp.h"
 #include"ast_ll_pp.h"
 
-bool macro_finder::is_macro(expr * n, app * & head, expr * & def) {
+bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
     if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
         return false;
     TRACE("macro_finder", tout << "processing: " << mk_pp(n, m_manager) << "\n";);
     expr * body        = to_quantifier(n)->get_expr();
     unsigned num_decls = to_quantifier(n)->get_num_decls();
-    return m_util.is_simple_macro(body, num_decls, head, def);
+    return m_util.is_ite_macro(body, num_decls, head, def);
 }
 
 /**
@@ -171,23 +171,20 @@ bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * con
     for (unsigned i = 0; i < num; i++) {
         expr * n       = exprs[i];
         proof * pr     = m_manager.proofs_enabled() ? prs[i] : 0;
-        expr_ref new_n(m_manager);
+        expr_ref new_n(m_manager), def(m_manager);
         proof_ref new_pr(m_manager);
         m_macro_manager.expand_macros(n, pr, new_n, new_pr);
-        app * head = 0;
-        expr * def = 0;
-        app * t    = 0;
+        app_ref head(m_manager), t(m_manager);
         if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) {
-            TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << mk_pp(new_n, m_manager) << "\n";);
+            TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";);
             found_new_macro = true;
         }
         else if (is_arith_macro(new_n, new_pr, new_exprs, new_prs)) {
-            TRACE("macro_finder_found", tout << "found new arith macro:\n" << mk_pp(new_n, m_manager) << "\n";);
+            TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";);
             found_new_macro = true;
         }
         else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) { 
-            TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << mk_pp(head, m_manager) << "\n" << mk_pp(t, m_manager) << "\n" << 
-                  mk_pp(def, m_manager) << "\n";);
+            TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";);
             pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_exprs, new_prs);
             found_new_macro = true;
         }
diff --git a/src/ast/macros/macro_finder.h b/src/ast/macros/macro_finder.h
index 541ec80b7..04ec11939 100644
--- a/src/ast/macros/macro_finder.h
+++ b/src/ast/macros/macro_finder.h
@@ -41,7 +41,7 @@ class macro_finder {
     bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
     bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
 
-    bool is_macro(expr * n, app * & head, expr * & def);
+    bool is_macro(expr * n, app_ref & head, expr_ref & def);
     bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t);
     bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def);
 
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index de55de632..4fb8b3db6 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -176,7 +176,7 @@ bool macro_util::is_macro_head(expr * n, unsigned num_decls) const {
    def  will contain t
 
 */
-bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app * & head, expr * & def) const {
+bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {
     if (m_manager.is_eq(n) || m_manager.is_iff(n)) {
         expr * lhs = to_app(n)->get_arg(0);
         expr * rhs = to_app(n)->get_arg(1);
@@ -189,6 +189,22 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app * & head
     return false;
 }
 
+bool macro_util::is_ite_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref& def) const {
+    if (is_simple_macro(n, num_decls, head, def)) {
+        return true;
+    }
+    expr* c, *t, *e;
+    expr_ref def1(m_manager), def2(m_manager);
+    app_ref head2(m_manager);
+    if (m_manager.is_ite(n, c, t, e) &&
+        is_ite_macro(t, num_decls, head,  def1) &&
+        is_ite_macro(e, num_decls, head2, def2) && head == head2) {
+        def = m_manager.mk_ite(c, def1, def2);
+        return true;
+    }
+    return false;
+}
+
 /**
    \brief Return true if n is of the form
    
@@ -206,7 +222,7 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app * & head
    def  will contain t
 
 */
-bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app * & head, expr * & def) const {
+bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {
     if (m_manager.is_eq(n) || m_manager.is_iff(n)) {
         expr * lhs = to_app(n)->get_arg(0);
         expr * rhs = to_app(n)->get_arg(1);
@@ -302,7 +318,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
 /**
    \brief Auxiliary function for is_pseudo_predicate_macro. It detects the pattern (= (f X) t)
 */
-bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t) {
+bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t) {
     if (!m_manager.is_eq(n)) 
         return false;
     expr * lhs = to_app(n)->get_arg(0);
@@ -332,7 +348,7 @@ bool macro_util::is_pseudo_head(expr * n, unsigned num_decls, app * & head, app
    \brief Returns true if n if of the form (forall (X) (iff (= (f X) t) def[X]))
    where t is a ground term, (f X) is the head. 
 */
-bool macro_util::is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def) {
+bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def) {
     if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
         return false;
     TRACE("macro_util", tout << "processing: " << mk_pp(n, m_manager) << "\n";);
@@ -870,9 +886,8 @@ void macro_util::collect_arith_macro_candidates(expr * atom, unsigned num_decls,
             THEN M'(atom) = true
 */
 void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls, macro_candidates & r) {
-    if (m_manager.is_eq(atom) || m_manager.is_iff(atom)) {
-        expr * lhs = to_app(atom)->get_arg(0);
-        expr * rhs = to_app(atom)->get_arg(1);
+    expr* lhs, *rhs;
+    if (m_manager.is_eq(atom, lhs, rhs) || m_manager.is_iff(atom, lhs, rhs)) {
         if (is_quasi_macro_head(lhs, num_decls) && 
             !is_forbidden(to_app(lhs)->get_decl()) && 
             !occurs(to_app(lhs)->get_decl(), rhs) &&
@@ -884,7 +899,6 @@ void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls,
         else if (is_hint_atom(lhs, rhs)) {
             insert_quasi_macro(to_app(lhs), num_decls, rhs, 0, false, true, true, r);
         }
-
         
         if (is_quasi_macro_head(rhs, num_decls) && 
             !is_forbidden(to_app(rhs)->get_decl()) && 
diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h
index 2a1581162..bb1b4777b 100644
--- a/src/ast/macros/macro_util.h
+++ b/src/ast/macros/macro_util.h
@@ -102,11 +102,12 @@ public:
     basic_simplifier_plugin * get_basic_simp() const;
 
     bool is_macro_head(expr * n, unsigned num_decls) const;
-    bool is_left_simple_macro(expr * n, unsigned num_decls, app * & head, expr * & def) const;
-    bool is_right_simple_macro(expr * n, unsigned num_decls, app * & head, expr * & def) const;
-    bool is_simple_macro(expr * n, unsigned num_decls, app * & head, expr * & def) const {
+    bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
+    bool is_right_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
+    bool is_simple_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref & def) const {
         return is_left_simple_macro(n, num_decls, head, def) || is_right_simple_macro(n, num_decls, head, def); 
     }
+    bool is_ite_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref& def) const;
 
     bool is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const;
     bool is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const {
@@ -114,8 +115,8 @@ public:
         return is_arith_macro(n, num_decls, head, def, inv);
     }
     
-    bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t);
-    bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def);
+    bool is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t);
+    bool is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def);
 
     bool is_quasi_macro_head(expr * n, unsigned num_decls) const;
     void quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls, app_ref & head, expr_ref & cond) const;
diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp
index a4d65d30b..14b2a6d32 100644
--- a/src/nlsat/tactic/nlsat_tactic.cpp
+++ b/src/nlsat/tactic/nlsat_tactic.cpp
@@ -25,6 +25,7 @@ Notes:
 #include"ast_smt2_pp.h"
 #include"z3_exception.h"
 #include"algebraic_numbers.h"
+#include"ast_pp.h"
 
 class nlsat_tactic : public tactic {
     struct expr_display_var_proc : public nlsat::display_var_proc {
@@ -78,9 +79,21 @@ class nlsat_tactic : public tactic {
             }
             return false;
         }
+
+        bool eval_model(model& model, goal& g) {
+            unsigned sz = g.size();
+            for (unsigned i = 0; i < sz; i++) {
+                expr_ref val(m);
+                if (model.eval(g.form(i), val) && !m.is_true(val)) {
+                    TRACE("nlsat", tout << mk_pp(g.form(i), m) << " -> " << val << "\n";);
+                    return false;
+                }
+            }
+            return true;
+        }
         
         // Return false if nlsat assigned noninteger value to an integer variable.
-        bool mk_model(expr_ref_vector & b2a, expr_ref_vector & x2t, model_converter_ref & mc) {
+        bool mk_model(goal & g, expr_ref_vector & b2a, expr_ref_vector & x2t, model_converter_ref & mc) {
             bool ok = true;
             model_ref md = alloc(model, m);
             arith_util util(m);
@@ -110,6 +123,7 @@ class nlsat_tactic : public tactic {
                     continue; // don't care
                 md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false());
             }
+            DEBUG_CODE(eval_model(*md.get(), g););
             mc = model2model_converter(md.get());
             return ok;
         }
@@ -151,7 +165,7 @@ class nlsat_tactic : public tactic {
                 if (!contains_unsupported(b2a, x2t)) {
                     // If mk_model is false it means that the model produced by nlsat 
                     // assigns noninteger values to integer variables
-                    if (mk_model(b2a, x2t, mc)) {
+                    if (mk_model(*g.get(), b2a, x2t, mc)) {
                         // result goal is trivially SAT
                         g->reset(); 
                     }
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 8e7765ee9..07d30222b 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1235,6 +1235,14 @@ namespace smt {
         ctx.set_var_theory(bv, get_id());
         rational _k;
         VERIFY(m_util.is_numeral(rhs, _k));
+        if (is_int(v) && !_k.is_int()) {
+            if (kind == A_UPPER) {
+                _k = floor(_k);
+            }
+            else {
+                _k = ceil(_k);
+            }
+        }
         inf_numeral   k(_k);
         atom * a = alloc(atom, bv, v, k, kind);
         mk_bound_axioms(a);
@@ -1399,22 +1407,22 @@ namespace smt {
         final_check_status result = FC_DONE;
         final_check_status ok;
         do {
-            TRACE("final_check_arith", tout << "m_final_check_idx: " << m_final_check_idx << ", result: " << result << "\n";);
+            TRACE("arith", tout << "m_final_check_idx: " << m_final_check_idx << ", result: " << result << "\n";);
             switch (m_final_check_idx) {
             case 0:
                 ok = check_int_feasibility();
-                TRACE("final_check_arith", tout << "check_int_feasibility(), ok: " << ok << "\n";);
+                TRACE("arith", tout << "check_int_feasibility(), ok: " << ok << "\n";);
                 break;
             case 1:
                 if (assume_eqs_core())
                     ok = FC_CONTINUE;
                 else
                     ok = FC_DONE;
-                TRACE("final_check_arith", tout << "assume_eqs(), ok: " << ok << "\n";);
+                TRACE("arith", tout << "assume_eqs(), ok: " << ok << "\n";);
                 break;
             default:
                 ok = process_non_linear();
-                TRACE("final_check_arith", tout << "non_linear(), ok: " << ok << "\n";);
+                TRACE("arith", tout << "non_linear(), ok: " << ok << "\n";);
                 break;
             }
             m_final_check_idx = (m_final_check_idx + 1) % 3;
@@ -1425,7 +1433,7 @@ namespace smt {
                 result = FC_GIVEUP;
                 break;
             case FC_CONTINUE:
-                TRACE("final_check_arith", 
+                TRACE("arith", 
                       tout << "continue arith..." 
                       << (get_context().inconsistent()?"inconsistent\n":"\n"););
                 return FC_CONTINUE;
@@ -1442,7 +1450,7 @@ namespace smt {
     template<typename Ext>
     final_check_status theory_arith<Ext>::final_check_eh() {
         TRACE("arith_eq_adapter_info", m_arith_eq_adapter.display_already_processed(tout););
-        TRACE("arith_final_check", display(tout););
+        TRACE("arith", display(tout););
 
         if (!propagate_core()) 
             return FC_CONTINUE; 
@@ -1459,7 +1467,7 @@ namespace smt {
         m_liberal_final_check = false;
         m_changed_assignment  = false;
         result = final_check_core();
-        TRACE("final_check_arith", tout << "result: " << result << "\n";);
+        TRACE("arith", tout << "result: " << result << "\n";);
         return result;
     }
     
@@ -2416,6 +2424,7 @@ namespace smt {
         theory_var          v = b->get_var();
         inf_numeral const & k = b->get_value();
 
+        TRACE("arith", display_bound(tout, b); tout << "v" << v << " <= " << k << "\n";);
         bound * u = upper(v);
         bound * l = lower(v);
         
@@ -2456,7 +2465,7 @@ namespace smt {
 
     template<typename Ext>
     bool theory_arith<Ext>::assert_bound(bound * b) {
-        TRACE("assert_bound", display_bound(tout, b););
+        TRACE("assert_bound", display_bound(tout, b); display(tout););
         theory_var v = b->get_var();
 
         if (b->is_atom()) {
@@ -2478,7 +2487,7 @@ namespace smt {
             break;
         }
         
-        TRACE("arith_assert", tout << "result: " << result << "\n"; display(tout););
+        TRACE("arith_bound", tout << "result: " << result << "\n"; display(tout););
         return result;
     }
 
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 72e1f1bc2..d3b1f0f10 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -1267,11 +1267,11 @@ namespace smt {
     final_check_status theory_arith<Ext>::check_int_feasibility() {
         TRACE("arith_int_detail", get_context().display(tout););
         if (!has_infeasible_int_var()) {
-            TRACE("arith_int_incomp", tout << "FC_DONE 1...\n"; display(tout););
+            TRACE("arith", tout << "FC_DONE 1...\n"; display(tout););
             return FC_DONE;
         }
 
-        TRACE("arith_int_fracs",
+        TRACE("arith",
               int num = get_num_vars();
               for (theory_var v = 0; v < num; v++) {
                   if (is_int(v) && !get_value(v).is_int()) {
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index f41eb017b..95cea5138 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -378,12 +378,13 @@ struct purify_arith_proc {
             cache_result(t, result, result_pr);
             
             expr * x = args[0];
-            // to-real(k) - x >= 0
-            expr * diff = u().mk_add(u().mk_to_real(k), u().mk_mul(u().mk_numeral(rational(-1), false), x));
+            // x - to-real(k) >= 0
+            
+            expr * diff = u().mk_add(x, u().mk_mul(u().mk_numeral(rational(-1), false), u().mk_to_real(k)));
             push_cnstr(u().mk_ge(diff, mk_real_zero()));
             push_cnstr_pr(result_pr);
             
-            // not(to-real(k) - x >= 1)
+            // not(x - to-real(k) >= 1)
             push_cnstr(NOT(u().mk_ge(diff, u().mk_numeral(rational(1), false))));
             push_cnstr_pr(result_pr);
         }
@@ -757,6 +758,7 @@ struct purify_arith_proc {
         
         // add cnstraints
         sz = r.cfg().m_new_cnstrs.size();
+        TRACE("purify_arith", tout << r.cfg().m_new_cnstrs << "\n";);
         for (unsigned i = 0; i < sz; i++) {
             m_goal.assert_expr(r.cfg().m_new_cnstrs.get(i), m_produce_proofs ? r.cfg().m_new_cnstr_prs.get(i) : 0, 0);
         }
@@ -827,6 +829,7 @@ public:
             SASSERT(g->is_well_sorted());
             mc = 0; pc = 0; core = 0;
             tactic_report report("purify-arith", *g);
+            TRACE("purify_arith", g->display(tout););
             bool produce_proofs = g->proofs_enabled();
             bool produce_models = g->models_enabled();
             bool elim_root_objs = m_params.get_bool("elim_root_objects", true);