diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index dd774772a..7e3ef87ed 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -126,6 +126,7 @@ bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_depen
     m_decl2macro_dep.insert(f, dep);
 
     TRACE("macro_insert", tout << "A macro was successfully created for: " << f->get_name() << "\n";);
+    SASSERT(false);
 
     // Nothing's forbidden anymore; if something's bad, we detected it earlier.
     // mark_forbidden(m->get_expr());
@@ -267,17 +268,19 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
         func_decl * d  = n->get_decl();
         TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
         if (mm.m_decl2macro.find(d, q)) {
-            TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";);
+            
             app * head = nullptr;
             expr * def = nullptr;
             mm.get_head_def(q, d, head, def);
             unsigned num = n->get_num_args();
             SASSERT(head && def);
+            TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n" << mk_pp(head, m) << " " << mk_pp(def, m) << "\n";);
             ptr_buffer<expr> subst_args;
             subst_args.resize(num, 0);
             for (unsigned i = 0; i < num; i++) {
                 var * v = to_var(head->get_arg(i));
-                SASSERT(v->get_idx() < num);
+                if (v->get_idx() >= num)
+                    return false;
                 unsigned nidx = num - v->get_idx() - 1;
                 SASSERT(subst_args[nidx] == 0);
                 subst_args[nidx] = n->get_arg(i);
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 3fae80e3e..b7b1efd39 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -436,6 +436,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl
    See normalize_expr
 */
 void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const {
+    TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n";);
     SASSERT(is_macro_head(head, head->get_num_args()));
     SASSERT(!occurs(head->get_decl(), def));
     normalize_expr(head, num_decls, def, interp);
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index a3130d565..d1c4a0045 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -25,7 +25,6 @@ Revision History:
 #include "ast/rewriter/th_rewriter.h"
 #include "tactic/generic_model_converter.h"
 #include "ast/arith_decl_plugin.h"
-#include "ast/seq_decl_plugin.h"
 #include "ast/expr_substitution.h"
 #include "ast/ast_smt2_pp.h"
 
@@ -35,7 +34,6 @@ class fix_dl_var_tactic : public tactic {
         struct failed {};
         ast_manager &          m;
         arith_util &           m_util;
-        seq_util               m_seq;
         expr_fast_mark1 *      m_visited;
         ptr_vector<expr>       m_todo;
         obj_map<app, unsigned> m_occs;
@@ -43,8 +41,7 @@ class fix_dl_var_tactic : public tactic {
 
         is_target(arith_util & u):
             m(u.get_manager()),
-            m_util(u),
-            m_seq(m) {
+            m_util(u){
         }
         
         void throw_failed(expr * ctx1, expr * ctx2 = nullptr) {
@@ -56,15 +53,6 @@ class fix_dl_var_tactic : public tactic {
             sort * s = m.get_sort(n);
             return s->get_family_id() == m_util.get_family_id();
         }
-        // Return true if n is uninterpreted with respect to arithmetic.
-        // sequence theory is not disjoint from arithmetic
-        bool is_uninterp(expr * n) {
-            if (!is_app(n)) return false;
-            app* t = to_app(n);
-            family_id fid = t->get_family_id();
-            return fid != m_util.get_family_id() && fid != m_seq.get_family_id();
-        }
-
         // Remark: we say an expression is nested, if it occurs inside the boolean structure of the formula.
         // That is, the expression is not part of an unit clause comprising of a single inequality/equality.