diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp
index bdc32e97c..a06d125a5 100644
--- a/src/ast/converters/expr_inverter.cpp
+++ b/src/ast/converters/expr_inverter.cpp
@@ -400,6 +400,7 @@ class bv_expr_inverter : public iexpr_inverter {
     }
 
     bool process_concat(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
+//        return false;
         if (num == 0)
             return false;
         if (!uncnstr(num, args))
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 231858897..c7cf2d11c 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -66,7 +66,6 @@ bool elim_unconstrained::is_var_lt(int v1, int v2) const {
 }
 
 void elim_unconstrained::eliminate() {
-
     while (!m_heap.empty()) {
         expr_ref r(m);
         int v = m_heap.erase_min();
@@ -86,7 +85,12 @@ void elim_unconstrained::eliminate() {
             n.m_refcount = 0;
             continue;
         }
+        if (m_heap.contains(root(e))) {
+            IF_VERBOSE(11, verbose_stream() << "already in heap " << mk_bounded_pp(e, m) << "\n");
+            continue;
+        }
         app* t = to_app(e);
+        TRACE("elim_unconstrained", tout << "eliminating " << mk_pp(t, m) << "\n";);
         unsigned sz = m_args.size();
         for (expr* arg : *to_app(t))
             m_args.push_back(reconstruct_term(get_node(arg)));
@@ -99,12 +103,15 @@ void elim_unconstrained::eliminate() {
             proof * pr  = m.mk_apply_def(s, r, pr1);
             m_trail.push_back(pr);
         }
+        expr_ref rr(m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz), m);
         n.m_refcount = 0;
         m_args.shrink(sz);
         if (!inverted) {
             IF_VERBOSE(11, verbose_stream() << "not inverted " << mk_bounded_pp(e, m) << "\n");
             continue;
         }
+
+        IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " / " << rr << " -> " << r << "\n");
         
         TRACE("elim_unconstrained", tout << mk_pp(t, m) << " -> " << r << "\n");
         SASSERT(r->get_sort() == t->get_sort());
@@ -119,7 +126,8 @@ void elim_unconstrained::eliminate() {
         get_node(e).m_term = r;
         get_node(e).m_proof = pr;
         get_node(e).m_refcount++;
-        IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(e, m) << "\n");
+        get_node(e).m_dirty = false;
+        IF_VERBOSE(11, verbose_stream() << "set " << &get_node(e) << " " << root(e) << " " << mk_bounded_pp(e, m) << " := " << mk_bounded_pp(r, m) << "\n");
         SASSERT(!m_heap.contains(root(e)));
         if (is_uninterp_const(r))
             m_heap.insert(root(e));
@@ -283,13 +291,22 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
     expr* t = n0.m_term;
     if (!n0.m_dirty)
         return expr_ref(t, m);
+    if (!is_node(t))
+        return expr_ref(t, m);
     ptr_vector<expr> todo;
     todo.push_back(t);
     while (!todo.empty()) {
         t = todo.back();
+        if (!is_node(t)) {
+            UNREACHABLE();
+        }
         node& n = get_node(t);
         unsigned sz0 = todo.size();
-        if (is_app(t)) {            
+        if (is_app(t)) {     
+            if (n.m_term != t) {
+                todo.pop_back();
+                continue;
+            }
             for (expr* arg : *to_app(t)) 
                 if (get_node(arg).m_dirty || !get_node(arg).m_term)
                     todo.push_back(arg);
@@ -300,7 +317,6 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
             for (expr* arg : *to_app(t)) 
                 m_args.push_back(get_node(arg).m_term);            
             n.m_term = m.mk_app(to_app(t)->get_decl(), to_app(t)->get_num_args(), m_args.data() + sz);
-
             m_args.shrink(sz);
         }
         else if (is_quantifier(t)) {
@@ -410,7 +426,7 @@ void elim_unconstrained::reduce() {
     generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
     m_inverter.set_model_converter(mc.get());
     m_created_compound = true;
-    for (unsigned rounds = 0; m_created_compound && rounds < 3; ++rounds) {
+    for (unsigned rounds = 0; m_created_compound && rounds < 1; ++rounds) {
         m_created_compound = false;
         init_nodes();
         eliminate();
diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp
index 95f73fd7a..47ebea525 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.cpp
+++ b/src/ast/simplifiers/model_reconstruction_trail.cpp
@@ -182,11 +182,11 @@ std::ostream& model_reconstruction_trail::display(std::ostream& out) const {
             out << "hide " << t->m_decl->get_name() << "\n";
         else if (t->is_def()) {
             for (auto const& [f, def, dep] : t->m_defs)
-                out << f->get_name() << " <- " << mk_pp(def, m) << "\n";
+                out << "def: " << f->get_name() << " <- " << mk_pp(def, m) << "\n";
         }            
         else {
             for (auto const& [v, def] : t->m_subst->sub())
-                out << mk_pp(v, m) << " <- " << mk_pp(def, m) << "\n";            
+                out << "sub: " << mk_pp(v, m) << " -> " << mk_pp(def, m) << "\n";
         }
         for (auto const& d : t->m_removed)
             out << "rm: " << d << "\n";
diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index 55ab4846c..d0ecff794 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -104,10 +104,10 @@ namespace intblast {
         ctx.push(push_back_vector(m_preds));
     }
 
-    void solver::set_translated(expr* e, expr* r) { 
+    void solver::set_translated(expr* e, expr* r) {
         SASSERT(r);
-        SASSERT(!is_translated(e));          
-        m_translate.setx(e->get_id(), r); 
+        SASSERT(!is_translated(e));
+        m_translate.setx(e->get_id(), r);
         ctx.push(set_vector_idx_trail(m_translate, e->get_id()));
     }
 
@@ -157,7 +157,7 @@ namespace intblast {
     bool solver::unit_propagate() {
         return add_bound_axioms() || add_predicate_axioms();
     }
-    
+
     void solver::ensure_translated(expr* e) {
         if (m_translate.get(e->get_id(), nullptr))
             return;
@@ -179,7 +179,7 @@ namespace intblast {
                 }
         }
         std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
-        for (expr* e : todo)            
+        for (expr* e : todo)
             translate_expr(e);
     }
 
@@ -335,7 +335,7 @@ namespace intblast {
             es[i] = translated(es.get(i));
     }
 
-    sat::check_result solver::check() { 
+    sat::check_result solver::check() {
         // ensure that bv2int is injective
         for (auto e : m_bv2int) {
             euf::enode* n = expr2enode(e);
@@ -347,10 +347,12 @@ namespace intblast {
                     continue;
                 if (sib->get_arg(0)->get_root() == r1)
                     continue;
-		auto a = eq_internalize(n, sib);
-		auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
-		ctx.mark_relevant(a);
-		ctx.mark_relevant(b);
+                if (sib->get_arg(0)->get_sort() != n->get_arg(0)->get_sort())
+                    continue;
+                auto a = eq_internalize(n, sib);
+                auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
+                ctx.mark_relevant(a);
+                ctx.mark_relevant(b);
                 add_clause(~a, b, nullptr);
                 return sat::check_result::CR_CONTINUE;
             }
@@ -368,13 +370,13 @@ namespace intblast {
             auto nBv2int = ctx.get_enode(bv2int);
             auto nxModN = ctx.get_enode(xModN);
             if (nBv2int->get_root() != nxModN->get_root()) {
-	      auto a = eq_internalize(nBv2int, nxModN);
-	      ctx.mark_relevant(a);
+                auto a = eq_internalize(nBv2int, nxModN);
+                ctx.mark_relevant(a);
                 add_unit(a);
                 return sat::check_result::CR_CONTINUE;
             }
         }
-        return sat::check_result::CR_DONE; 
+        return sat::check_result::CR_DONE;
     }
 
     expr* solver::umod(expr* bv_expr, unsigned i) {
@@ -482,8 +484,8 @@ namespace intblast {
                 m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i));
 
         if (has_bv_sort)
-            m_vars.push_back(e);        
-        
+            m_vars.push_back(e);
+
         if (m_is_plugin) {
             expr* r = m.mk_app(f, m_args);
             if (has_bv_sort) {
@@ -504,7 +506,7 @@ namespace intblast {
             f = g;
             m_pinned.push_back(f);
         }
-        set_translated(e, m.mk_app(f, m_args));        
+        set_translated(e, m.mk_app(f, m_args));
     }
 
     void solver::translate_bv(app* e) {
@@ -536,7 +538,7 @@ namespace intblast {
                 r = a.mk_add(hi, lo);
             }
             return r;
-        };
+            };
 
         expr* bv_expr = e;
         expr* r = nullptr;
@@ -634,22 +636,22 @@ namespace intblast {
             break;
         }
         case OP_BSHL: {
-            if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1))) 
-                r = a.mk_shl(bv.get_bv_size(e), arg(0),arg(1));
+            if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))
+                r = a.mk_shl(bv.get_bv_size(e), arg(0), arg(1));
             else {
                 expr* x = arg(0), * y = umod(e, 1);
                 r = a.mk_int(0);
                 IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
                 for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
-                    r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r);   
+                    r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r);
             }
             break;
         }
         case OP_BNOT:
             r = bnot(arg(0));
             break;
-        case OP_BLSHR: 
-            if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))  
+        case OP_BLSHR:
+            if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))
                 r = a.mk_lshr(bv.get_bv_size(e), arg(0), arg(1));
             else {
                 expr* x = arg(0), * y = umod(e, 1);
@@ -659,11 +661,11 @@ namespace intblast {
                     r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
             }
             break;
-        case OP_BASHR: 
+        case OP_BASHR:
             if (!a.is_numeral(arg(1)))
                 r = a.mk_ashr(bv.get_bv_size(e), arg(0), arg(1));
             else {
-                
+
                 //
                 // ashr(x, y)
                 // if y = k & x >= 0 -> x / 2^k   
@@ -671,15 +673,15 @@ namespace intblast {
                 //
                 unsigned sz = bv.get_bv_size(e);
                 rational N = bv_size(e);
-                expr* x = umod(e, 0), *y = umod(e, 1);
+                expr* x = umod(e, 0), * y = umod(e, 1);
                 expr* signx = a.mk_ge(x, a.mk_int(N / 2));
-                r = m.mk_ite(signx, a.mk_int(- 1), a.mk_int(0));
+                r = m.mk_ite(signx, a.mk_int(-1), a.mk_int(0));
                 IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
                 for (unsigned i = 0; i < sz; ++i) {
-                    expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));              
+                    expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));
                     r = m.mk_ite(m.mk_eq(y, a.mk_int(i)),
-                                 m.mk_ite(signx, a.mk_add(d, a.mk_int(- rational::power_of_two(sz-i))), d),
-                                 r);
+                        m.mk_ite(signx, a.mk_add(d, a.mk_int(-rational::power_of_two(sz - i))), d),
+                        r);
                 }
             }
             break;
@@ -744,11 +746,11 @@ namespace intblast {
             r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0));
             break;
         case OP_BSMOD_I:
-        case OP_BSMOD: {            
-            expr* x = umod(e, 0), *y = umod(e, 1);
-            rational N = bv_size(e); 
-            expr* signx = a.mk_ge(x, a.mk_int(N/2));
-            expr* signy = a.mk_ge(y, a.mk_int(N/2));
+        case OP_BSMOD: {
+            expr* x = umod(e, 0), * y = umod(e, 1);
+            rational N = bv_size(e);
+            expr* signx = a.mk_ge(x, a.mk_int(N / 2));
+            expr* signy = a.mk_ge(y, a.mk_int(N / 2));
             expr* u = a.mk_mod(x, y);
             // u = 0 ->  0
             // y = 0 ->  x
@@ -756,14 +758,14 @@ namespace intblast {
             // x < 0, y >= 0 ->  y - u
             // x >= 0, y < 0 ->  y + u
             // x >= 0, y >= 0 ->  u
-            r = a.mk_uminus(u);   
+            r = a.mk_uminus(u);
             r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), a.mk_add(u, y), r);
             r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r);
             r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r);
             r = m.mk_ite(m.mk_eq(u, a.mk_int(0)), a.mk_int(0), r);
             r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
             break;
-        } 
+        }
         case OP_BSDIV_I:
         case OP_BSDIV: {
             // d = udiv(abs(x), abs(y))
@@ -799,7 +801,7 @@ namespace intblast {
             d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
             r = a.mk_sub(x, a.mk_mul(d, y));
             r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
-            break;  
+            break;
         }
         case OP_ROTATE_LEFT: {
             auto n = e->get_parameter(0).get_int();
@@ -812,11 +814,11 @@ namespace intblast {
             r = rotate_left(sz - n);
             break;
         }
-        case OP_EXT_ROTATE_LEFT:  {
+        case OP_EXT_ROTATE_LEFT: {
             unsigned sz = bv.get_bv_size(e);
             expr* y = umod(e, 1);
             r = a.mk_int(0);
-            for (unsigned i = 0; i < sz; ++i) 
+            for (unsigned i = 0; i < sz; ++i)
                 r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r);
             break;
         }
@@ -824,7 +826,7 @@ namespace intblast {
             unsigned sz = bv.get_bv_size(e);
             expr* y = umod(e, 1);
             r = a.mk_int(0);
-            for (unsigned i = 0; i < sz; ++i) 
+            for (unsigned i = 0; i < sz; ++i)
                 r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r);
             break;
         }
@@ -837,7 +839,7 @@ namespace intblast {
             for (unsigned i = 1; i < n; ++i)
                 r = a.mk_add(a.mk_mul(a.mk_int(N), x), r), N *= N0;
             break;
-        }            
+        }
         case OP_BREDOR: {
             r = umod(e->get_arg(0), 0);
             r = m.mk_not(m.mk_eq(r, a.mk_int(0)));
@@ -897,7 +899,7 @@ namespace intblast {
     }
 
     bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
-      if (!is_app(n->get_expr()))
+        if (!is_app(n->get_expr()))
             return false;
         app* e = to_app(n->get_expr());
         if (n->num_args() == 0) {
@@ -916,7 +918,7 @@ namespace intblast {
     void solver::add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values) {
         expr* e = n->get_expr();
         SASSERT(bv.is_bv(e));
-        
+
         if (bv.is_numeral(e)) {
             values.setx(n->get_root_id(), e);
             return;
@@ -957,7 +959,6 @@ namespace intblast {
             rational r;
             VERIFY(av.get_value(b2i->get_expr(), r));
             value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr()));
-            verbose_stream() << ctx.bpp(n) << " := " << value << "\n";
         }
         values.set(n->get_root_id(), value);
         TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n");
@@ -981,9 +982,8 @@ namespace intblast {
                     continue;
                 verbose_stream() << "value mismatch : " << mk_bounded_pp(e, m) << " := " << val1 << "\n";
                 verbose_stream() << mk_bounded_pp(f, m) << " := " << r2 << "\n";
-                for (expr* arg : *to_app(e)) {
+                for (expr* arg : *to_app(e)) 
                     verbose_stream() << mk_bounded_pp(arg, m) << " := " << mdl(arg) << "\n";
-                }
             }
         }
     }