diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
index 6bdd34626..fa4bbdd49 100644
--- a/src/ast/simplifiers/dependent_expr_state.h
+++ b/src/ast/simplifiers/dependent_expr_state.h
@@ -61,9 +61,9 @@ public:
  */
 class dependent_expr_simplifier {
 protected:
-    ast_manager&          m;
+    ast_manager& m;
     dependent_expr_state& m_fmls;
-    trail_stack&          m_trail;
+    trail_stack& m_trail;
     unsigned              m_qhead = 0;          // pointer into last processed formula in m_fmls
 
     unsigned num_scopes() const { return m_trail.get_num_scopes(); }
@@ -78,6 +78,7 @@ public:
     virtual void collect_statistics(statistics& st) const {}
     virtual void reset_statistics() {}
     virtual void updt_params(params_ref const& p) {}
+    virtual void collect_param_descrs(param_descrs& r) {}
 };
 
 /**
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index d0eb2a53f..d590f3e59 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -47,11 +47,9 @@ Author:
 
 elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) :
     dependent_expr_simplifier(m, fmls), m_inverter(m), m_lt(*this), m_heap(1024, m_lt), m_trail(m) {
-
     std::function<bool(expr*)> is_var = [&](expr* e) {
-        return is_uninterp_const(e) && !m_frozen.is_marked(e) && get_node(e).m_refcount == 1;
+        return is_uninterp_const(e) && !m_frozen.is_marked(e) && get_node(e).m_refcount <= 1;
     };
-
     m_inverter.set_is_var(is_var);
 }
 
@@ -61,7 +59,6 @@ bool elim_unconstrained::is_var_lt(int v1, int v2) const {
     return n1.m_refcount < n2.m_refcount;
 }
 
-
 void elim_unconstrained::eliminate() {
 
     while (!m_heap.empty()) {
@@ -79,8 +76,7 @@ void elim_unconstrained::eliminate() {
             continue;
         }
         expr* e = get_parent(v);
-        for (expr* p : n.m_parents)
-            IF_VERBOSE(11, verbose_stream() << "parent " << mk_bounded_pp(p, m) << "\n");
+        IF_VERBOSE(11, for (expr* p : n.m_parents) verbose_stream() << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";);
         if (!e || !is_app(e) || !is_ground(e)) {
             n.m_refcount = 0;
             continue;
@@ -90,6 +86,7 @@ void elim_unconstrained::eliminate() {
         for (expr* arg : *to_app(t))
             m_args.push_back(get_node(arg).m_term);
         if (!m_inverter(t->get_decl(), m_args.size(), m_args.data(), r, side_cond)) {
+            IF_VERBOSE(11, verbose_stream() << "not inverted " << mk_bounded_pp(e, m) << "\n");
             n.m_refcount = 0;
             continue;
         }
@@ -103,12 +100,12 @@ void elim_unconstrained::eliminate() {
         m_root.setx(r->get_id(), e->get_id(), UINT_MAX);
         get_node(e).m_term = r;
         get_node(e).m_refcount++;
-        IF_VERBOSE(11, verbose_stream() << mk_pp(e, m) << "\n");
-        SASSERT(!m_heap.contains(e->get_id()));
+        IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(e, m) << "\n");
+        SASSERT(!m_heap.contains(root(e)));
         if (is_uninterp_const(r)) 
-            m_heap.insert(e->get_id());                    
+            m_heap.insert(root(e));                    
 
-        IF_VERBOSE(11, verbose_stream() << mk_pp(n.m_orig, m) << " " << mk_pp(t, m) << " -> " << r << " " << get_node(e).m_refcount << "\n");
+        IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(n.m_orig, m) << " " << mk_bounded_pp(t, m) << " -> " << r << " " << get_node(e).m_refcount << "\n";);
 
         SASSERT(!side_cond && "not implemented to add side conditions\n");
     }
@@ -178,7 +175,7 @@ void elim_unconstrained::init_terms(expr_ref_vector const& terms) {
         n.m_term = e;
         n.m_refcount = 0;
         if (is_uninterp_const(e))
-            m_heap.insert(e->get_id());
+            m_heap.insert(root(e));
         if (is_quantifier(e)) {
             expr* body = to_quantifier(e)->get_expr();
             get_node(body).m_parents.push_back(e);
diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h
index b32ab367b..89f28fe33 100644
--- a/src/ast/simplifiers/elim_unconstrained.h
+++ b/src/ast/simplifiers/elim_unconstrained.h
@@ -23,9 +23,9 @@ Author:
 class elim_unconstrained : public dependent_expr_simplifier {
 
     struct node {
-        unsigned         m_refcount;
-        expr*            m_term;
-        expr*            m_orig;
+        unsigned         m_refcount = 0;
+        expr*            m_term = nullptr;
+        expr*            m_orig = nullptr;
         ptr_vector<expr> m_parents;
     };
     struct var_lt {
@@ -52,11 +52,12 @@ class elim_unconstrained : public dependent_expr_simplifier {
     bool is_var_lt(int v1, int v2) const;
     node& get_node(unsigned n) { return m_nodes[n]; }
     node const& get_node(unsigned n) const { return m_nodes[n]; }
-    node& get_node(expr* t) { return m_nodes[m_root[t->get_id()]]; }
-    node const& get_node(expr* t) const { return m_nodes[m_root[t->get_id()]]; }
+    node& get_node(expr* t) { return m_nodes[root(t)]; }
+    unsigned root(expr* t) const { return m_root[t->get_id()]; }
+    node const& get_node(expr* t) const { return m_nodes[root(t)]; }
     unsigned get_refcount(expr* t) const { return get_node(t).m_refcount; }
-    void inc_ref(expr* t) { ++get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.increased(t->get_id()); }
-    void dec_ref(expr* t) { --get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.decreased(t->get_id()); }
+    void inc_ref(expr* t) { ++get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.increased(root(t)); }
+    void dec_ref(expr* t) { --get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.decreased(root(t)); }
     void gc(expr* t);
     expr* get_parent(unsigned n) const;
     void init_terms(expr_ref_vector const& terms);
diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp
index 96b0427f6..0b6f12160 100644
--- a/src/ast/simplifiers/solve_eqs.cpp
+++ b/src/ast/simplifiers/solve_eqs.cpp
@@ -240,6 +240,13 @@ namespace euf {
             ex->updt_params(p);
     }
 
+    void solve_eqs::collect_param_descrs(param_descrs& r) {
+        r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.");
+        r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers.");
+        r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver.");
+        r.insert("context_solve", CPK_BOOL, "(default: false) solve equalities under disjunctions.");
+    }
+
     void solve_eqs::collect_statistics(statistics& st) const {
         st.update("solve-eqs-steps", m_stats.m_num_steps);
         st.update("solve-eqs-elim-vars", m_stats.m_num_elim_vars);
diff --git a/src/ast/simplifiers/solve_eqs.h b/src/ast/simplifiers/solve_eqs.h
index 8f5988a38..a2afd6e58 100644
--- a/src/ast/simplifiers/solve_eqs.h
+++ b/src/ast/simplifiers/solve_eqs.h
@@ -72,6 +72,8 @@ namespace euf {
 
         void updt_params(params_ref const& p) override;
 
+        void collect_param_descrs(param_descrs& r) override;
+
         void collect_statistics(statistics& st) const override;
 
     };
diff --git a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp
index e41347c2b..fc812c4f5 100644
--- a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp
+++ b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp
@@ -27,7 +27,6 @@ Notes:
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_term_ite_tactic.h"
 
 tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) {
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 66a391cb8..5895643bd 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -31,7 +31,6 @@ Notes:
 #include "tactic/tactic.h"
 #include "tactic/arith/lia2card_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt
index bab61afce..6bb6793fd 100644
--- a/src/tactic/core/CMakeLists.txt
+++ b/src/tactic/core/CMakeLists.txt
@@ -18,7 +18,6 @@ z3_add_component(core_tactics
     propagate_values_tactic.cpp
     reduce_args_tactic.cpp
     simplify_tactic.cpp
-    solve_eqs_tactic.cpp
     special_relations_tactic.cpp
     split_clause_tactic.cpp
     symmetry_reduce_tactic.cpp
@@ -48,7 +47,6 @@ z3_add_component(core_tactics
     reduce_args_tactic.h
     simplify_tactic.h
     solve_eqs_tactic.h
-    solve_eqs2_tactic.h
     special_relations_tactic.h
     split_clause_tactic.h
     symmetry_reduce_tactic.h
diff --git a/src/tactic/core/elim_uncnstr2_tactic.h b/src/tactic/core/elim_uncnstr2_tactic.h
index 2c5f81d5e..65b5d3426 100644
--- a/src/tactic/core/elim_uncnstr2_tactic.h
+++ b/src/tactic/core/elim_uncnstr2_tactic.h
@@ -30,7 +30,7 @@ public:
 };
 
 inline tactic * mk_elim_uncnstr2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
-    return alloc(dependent_expr_state_tactic, m, p, alloc(elim_uncnstr2_tactic_factory), "elim-unconstr2");
+    return alloc(dependent_expr_state_tactic, m, p, alloc(elim_uncnstr2_tactic_factory), "elim-uncnstr2");
 }
 
 
diff --git a/src/tactic/core/solve_eqs2_tactic.h b/src/tactic/core/solve_eqs2_tactic.h
deleted file mode 100644
index 7d13b571e..000000000
--- a/src/tactic/core/solve_eqs2_tactic.h
+++ /dev/null
@@ -1,47 +0,0 @@
-/*++
-Copyright (c) 2022 Microsoft Corporation
-
-Module Name:
-
-    solve_eqs2_tactic.h
-
-Abstract:
-
-    Tactic for solving variables
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2022-10-30
-
---*/
-#pragma once
-
-#include "util/params.h"
-#include "tactic/tactic.h"
-#include "tactic/dependent_expr_state_tactic.h"
-#include "ast/simplifiers/solve_eqs.h"
-
-
-class solve_eqs2_tactic_factory : public dependent_expr_simplifier_factory {
-public:
-    dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override {
-        return alloc(euf::solve_eqs, m, s);
-    }
-};
-
-inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p = params_ref()) {
-    return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs");
-}
-
-#if 1
-inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
-    return mk_solve_eqs2_tactic(m, p);
-}
-#endif
-
-
-/*
-  ADD_TACTIC("solve-eqs2", "solve for variables.", "mk_solve_eqs2_tactic(m, p)")
-*/
-
-
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
deleted file mode 100644
index d445b68ac..000000000
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ /dev/null
@@ -1,1109 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
-    solve_eqs_tactic.cpp
-
-Abstract:
-
-    Tactic for solving equations and performing gaussian elimination.
-
-Author:
-
-    Leonardo de Moura (leonardo) 2011-12-29.
-
-Revision History:
-
---*/
-#include "ast/rewriter/expr_replacer.h"
-#include "ast/occurs.h"
-#include "ast/ast_util.h"
-#include "ast/ast_pp.h"
-#include "ast/pb_decl_plugin.h"
-#include "ast/recfun_decl_plugin.h"
-#include "ast/rewriter/th_rewriter.h"
-#include "ast/rewriter/rewriter_def.h"
-#include "ast/rewriter/hoist_rewriter.h"
-#include "tactic/goal_shared_occs.h"
-#include "tactic/tactical.h"
-#include "ast/converters/generic_model_converter.h"
-#include "params/tactic_params.hpp"
-
-class solve_eqs_tactic : public tactic {
-    struct imp {
-        typedef generic_model_converter gmc;
-        
-        ast_manager &                 m_manager;
-        expr_replacer *               m_r;
-        params_ref                    m_params;
-        bool                          m_r_owner;
-        arith_util                    m_a_util;
-        obj_map<expr, unsigned>       m_num_occs;
-        unsigned                      m_num_steps;
-        unsigned                      m_num_eliminated_vars;
-        bool                          m_theory_solver;
-        bool                          m_ite_solver;
-        unsigned                      m_max_occs;
-        bool                          m_context_solve;
-        scoped_ptr<expr_substitution> m_subst;
-        scoped_ptr<expr_substitution> m_norm_subst;
-        expr_sparse_mark              m_candidate_vars;
-        expr_sparse_mark              m_candidate_set;
-        ptr_vector<expr>              m_candidates;
-        expr_ref_vector               m_marked_candidates;
-        ptr_vector<app>               m_vars;
-        expr_sparse_mark              m_nonzero;
-        ptr_vector<app>               m_ordered_vars;
-        bool                          m_produce_proofs;
-        bool                          m_produce_unsat_cores;
-        bool                          m_produce_models;
-        
-        imp(ast_manager & m, params_ref const & p, expr_replacer * r, bool owner):
-            m_manager(m),
-            m_r(r),
-            m_r_owner(r == nullptr || owner),
-            m_a_util(m),
-            m_num_steps(0),
-            m_num_eliminated_vars(0),
-            m_marked_candidates(m),
-            m_var_trail(m) {
-            updt_params(p);
-            if (m_r == nullptr)
-                m_r = mk_default_expr_replacer(m, true);
-        }
-        
-        ~imp() {
-            if (m_r_owner)
-                dealloc(m_r);
-        }
-        
-        ast_manager & m() const { return m_manager; }
-        
-        void updt_params(params_ref const & p) {
-            m_params.append(p);
-            tactic_params tp(m_params);
-            m_ite_solver     = p.get_bool("ite_solver", tp.solve_eqs_ite_solver());
-            m_theory_solver  = p.get_bool("theory_solver", tp.solve_eqs_theory_solver());
-            m_max_occs       = p.get_uint("solve_eqs_max_occs", tp.solve_eqs_max_occs());
-            m_context_solve  = p.get_bool("context_solve", tp.solve_eqs_context_solve());
-        }
-                
-        void checkpoint() {
-            tactic::checkpoint(m());
-        }
-        
-        // Check if the number of occurrences of t is below the specified threshold :solve-eqs-max-occs
-        bool check_occs(expr * t) const {
-            if (m_max_occs == UINT_MAX)
-                return true;
-            unsigned num = 0;
-            m_num_occs.find(t, num);
-            TRACE("solve_eqs_check_occs", tout << mk_ismt2_pp(t, m_manager) << " num_occs: " << num << " max: " << m_max_occs << "\n";);
-            return num <= m_max_occs;
-        }
-        
-        // Use: (= x def) and (= def x)
-
-        bool trivial_solve1(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) { 
-
-            if (is_uninterp_const(lhs) && !m_candidate_vars.is_marked(lhs) && !occurs(lhs, rhs) && check_occs(lhs)) {
-                var = to_app(lhs); 
-                def = rhs;
-                pr  = nullptr;
-                return true;
-            }
-            else {
-                return false;
-            }
-        }
-        bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
-            if (trivial_solve1(lhs, rhs, var, def, pr)) 
-                return true;
-            if (trivial_solve1(rhs, lhs, var, def, pr)) {
-                if (m_produce_proofs) {
-                    pr = m().mk_commutativity(m().mk_eq(lhs, rhs));
-                }
-                return true;
-            }
-            return false;
-        }
-        
-        // (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2))
-        bool solve_ite_core(app * ite, expr * lhs1, expr * rhs1, expr * lhs2, expr * rhs2, app_ref & var, expr_ref & def, proof_ref & pr) {
-            if (lhs1 != lhs2)
-                return false;
-            if (!is_uninterp_const(lhs1) || m_candidate_vars.is_marked(lhs1))
-                return false;
-            if (occurs(lhs1, ite->get_arg(0)) || occurs(lhs1, rhs1) || occurs(lhs1, rhs2))
-                return false;
-            if (!check_occs(lhs1))
-                return false;
-            var = to_app(lhs1);
-            def = m().mk_ite(ite->get_arg(0), rhs1, rhs2);
-            
-            if (m_produce_proofs)
-                pr = m().mk_rewrite(ite, m().mk_eq(var, def));
-            return true;
-        }
-        
-        // (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2))
-        bool solve_ite(app * ite, app_ref & var, expr_ref & def, proof_ref & pr) {
-            expr * t = ite->get_arg(1);
-            expr * e = ite->get_arg(2);
-            
-            if (!m().is_eq(t) || !m().is_eq(e))
-                return false;
-            
-            expr * lhs1 = to_app(t)->get_arg(0);
-            expr * rhs1 = to_app(t)->get_arg(1);
-            expr * lhs2 = to_app(e)->get_arg(0);
-            expr * rhs2 = to_app(e)->get_arg(1);
-            
-            return 
-                solve_ite_core(ite, lhs1, rhs1, lhs2, rhs2, var, def, pr) ||
-                solve_ite_core(ite, rhs1, lhs1, lhs2, rhs2, var, def, pr) ||
-                solve_ite_core(ite, lhs1, rhs1, rhs2, lhs2, var, def, pr) ||
-                solve_ite_core(ite, rhs1, lhs1, rhs2, lhs2, var, def, pr);
-        }
-        
-        bool is_pos_literal(expr * n) {
-            return is_app(n) && to_app(n)->get_num_args() == 0 && to_app(n)->get_family_id() == null_family_id;
-        }
-        
-        bool is_neg_literal(expr * n) {
-            if (m_manager.is_not(n))
-                return is_pos_literal(to_app(n)->get_arg(0));
-            return false;
-        }
-        
-        
-        /**
-           \brief Given t of the form (f s_0 ... s_n), 
-           return true if x occurs in some s_j for j != i 
-        */
-        bool occurs_except(expr * x, app * t, unsigned i) {
-            unsigned num = t->get_num_args();
-            for (unsigned j = 0; j < num; j++) {
-                if (i != j && occurs(x, t->get_arg(j)))
-                    return true;
-            }
-            return false;
-        }
-
-        void add_pos(expr* f) {
-            expr* lhs = nullptr, *rhs = nullptr;
-            rational val;
-            if (m_a_util.is_le(f, lhs, rhs) && m_a_util.is_numeral(rhs, val) && val.is_neg()) {
-                m_nonzero.mark(lhs);
-            }
-            else if (m_a_util.is_ge(f, lhs, rhs) && m_a_util.is_numeral(rhs, val) && val.is_pos()) {
-                m_nonzero.mark(lhs);
-            }
-            else if (m().is_not(f, f)) {
-                if (m_a_util.is_le(f, lhs, rhs) && m_a_util.is_numeral(rhs, val) && !val.is_neg()) {
-                    m_nonzero.mark(lhs);
-                }
-                else if (m_a_util.is_ge(f, lhs, rhs) && m_a_util.is_numeral(rhs, val) && !val.is_pos()) {
-                    m_nonzero.mark(lhs);
-                }
-                else if (m().is_eq(f, lhs, rhs) && m_a_util.is_numeral(rhs, val) && val.is_zero()) {
-                    m_nonzero.mark(lhs);                    
-                }
-            }            
-        }
-
-        bool is_nonzero(expr* e) {
-            return m_nonzero.is_marked(e);
-        }
-
-        bool isolate_var(app* arg, app_ref& var, expr_ref& div, unsigned i, app* lhs, expr* rhs) {
-            if (!m_a_util.is_mul(arg)) return false;
-            unsigned n = arg->get_num_args();
-            for (unsigned j = 0; j < n; ++j) {
-                expr* e = arg->get_arg(j);
-                bool ok = is_uninterp_const(e) && check_occs(e) && !occurs(e, rhs) && !occurs_except(e, lhs, i);
-                if (!ok) continue;
-                var = to_app(e);
-                for (unsigned k = 0; ok && k < n; ++k) {
-                    expr* arg_k = arg->get_arg(k);
-                    ok = k == j || (!occurs(var, arg_k) && is_nonzero(arg_k));
-                }
-                if (!ok) continue;
-                ptr_vector<expr> args;
-                for (unsigned k = 0; k < n; ++k) {
-                    if (k != j) args.push_back(arg->get_arg(k));
-                }
-                div = m_a_util.mk_mul(args.size(), args.data());
-                return true;
-            }
-            return false;
-        }
-
-        bool solve_nl(app * lhs, expr * rhs, expr* eq, app_ref& var, expr_ref & def, proof_ref & pr) {
-            SASSERT(m_a_util.is_add(lhs));
-            if (m_a_util.is_int(lhs)) return false;
-            unsigned num = lhs->get_num_args();
-            expr_ref div(m());
-            for (unsigned i = 0; i < num; i++) {
-                expr * arg = lhs->get_arg(i);
-                if (is_app(arg) && isolate_var(to_app(arg), var, div, i, lhs, rhs)) {
-                    ptr_vector<expr> args;
-                    for (unsigned k = 0; k < num; ++k) {
-                        if (k != i) args.push_back(lhs->get_arg(k));
-                    }
-                    def = m_a_util.mk_sub(rhs, m_a_util.mk_add(args.size(), args.data()));
-                    def = m_a_util.mk_div(def, div);
-                    if (m_produce_proofs)
-                        pr = m().mk_rewrite(eq, m().mk_eq(var, def));
-                    return true;
-                }
-            }
-            return false;
-        }
-        
-        bool solve_arith_core(app * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
-            SASSERT(m_a_util.is_add(lhs));
-            bool is_int  = m_a_util.is_int(lhs);
-            expr * a = nullptr; 
-            expr * v = nullptr;
-            rational a_val;
-            unsigned num = lhs->get_num_args();
-            unsigned i;
-            for (i = 0; i < num; i++) {
-                expr * arg = lhs->get_arg(i);
-                if (is_uninterp_const(arg) && !m_candidate_vars.is_marked(arg) && check_occs(arg) && !occurs(arg, rhs) && !occurs_except(arg, lhs, i)) {
-                    a_val = rational(1); 
-                    v     = arg;
-                    break;
-                }
-                else if (m_a_util.is_mul(arg, a, v) && 
-                         is_uninterp_const(v) && 
-                         !m_candidate_vars.is_marked(v) &&
-                         m_a_util.is_numeral(a, a_val) &&
-                         !a_val.is_zero() &&
-                         (!is_int || a_val.is_minus_one()) &&
-                         check_occs(v) &&
-                         !occurs(v, rhs) && 
-                         !occurs_except(v, lhs, i)) {
-                    break;
-                }
-            }
-            if (i == num)
-                return false;
-            var = to_app(v);
-            expr_ref inv_a(m());
-            if (!a_val.is_one()) {
-                inv_a = m_a_util.mk_numeral(rational(1)/a_val, is_int);
-                rhs   = m_a_util.mk_mul(inv_a, rhs);
-            }
-            
-            ptr_buffer<expr> other_args;
-            for (unsigned j = 0; j < num; j++) {
-                if (i != j) {
-                    if (inv_a)
-                        other_args.push_back(m_a_util.mk_mul(inv_a, lhs->get_arg(j)));
-                    else
-                        other_args.push_back(lhs->get_arg(j));
-                }
-            }
-            switch (other_args.size()) {
-            case 0:
-                def = rhs;
-                break;
-            case 1:
-                def = m_a_util.mk_sub(rhs, other_args[0]);
-                break;
-            default:
-                def = m_a_util.mk_sub(rhs, m_a_util.mk_add(other_args.size(), other_args.data()));
-                break;
-            }
-            if (m_produce_proofs)
-                pr = m().mk_rewrite(eq, m().mk_eq(var, def));
-            return true;
-        }
-
-        bool solve_mod(expr * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
-            rational r1, r2;
-            expr* arg1;
-            if (m_produce_proofs) 
-                return false;
-
-            auto fresh = [&]() { return m().mk_fresh_const("mod", m_a_util.mk_int()); };
-            auto mk_int = [&](rational const& r) { return m_a_util.mk_int(r); };
-            auto add = [&](expr* a, expr* b) { return m_a_util.mk_add(a, b); };
-            auto mul = [&](expr* a, expr* b) { return m_a_util.mk_mul(a, b); };
-
-            VERIFY(m_a_util.is_mod(lhs, lhs, arg1));
-            if (!m_a_util.is_numeral(arg1, r1) || !r1.is_pos()) {
-                return false;
-            }
-            // 
-            // solve lhs mod r1 = r2
-            // as lhs = r1*mod!1 + r2
-            // 
-            if (m_a_util.is_numeral(rhs, r2) && !r2.is_neg() && r2 < r1) {
-                expr_ref def0(m());
-                def0 = add(mk_int(r2), mul(fresh(), mk_int(r1)));
-                return solve_eq(lhs, def0, eq, var, def, pr);
-            }
-            return false;
-        }
-        
-        bool solve_arith(expr * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
-            return 
-                (m_a_util.is_add(lhs) && solve_arith_core(to_app(lhs), rhs, eq, var, def, pr)) ||
-                (m_a_util.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, var, def, pr)) ||
-                (m_a_util.is_mod(lhs) && solve_mod(lhs, rhs, eq, var, def, pr)) ||
-                (m_a_util.is_mod(rhs) && solve_mod(rhs, lhs, eq, var, def, pr));                 
-        }
-
-                
-        bool solve_eq(expr* arg1, expr* arg2, expr* eq, app_ref& var, expr_ref & def, proof_ref& pr) {
-            if (trivial_solve(arg1, arg2, var, def, pr))
-                return true;
-            if (m_theory_solver) {
-                if (solve_arith(arg1, arg2, eq, var, def, pr))
-                    return true;
-            }
-            return false;
-        }
-        
-        bool solve(expr * f, app_ref & var, expr_ref & def, proof_ref & pr) {
-            expr* arg1 = nullptr, *arg2 = nullptr;
-            if (m().is_eq(f, arg1, arg2)) {
-                return solve_eq(arg1, arg2, f, var, def, pr);
-            }
-                                    
-            if (m_ite_solver && m().is_ite(f))
-                return solve_ite(to_app(f), var, def, pr);
-            
-            if (is_pos_literal(f)) {
-                if (m_candidate_vars.is_marked(f))
-                    return false;
-                var = to_app(f);
-                def = m().mk_true();
-                if (m_produce_proofs) {
-                    // [rewrite]: (iff (iff l true) l)
-                    // [symmetry T1]: (iff l (iff l true))
-                    pr = m().mk_rewrite(m().mk_eq(var, def), var);
-                    pr = m().mk_symmetry(pr);
-                }
-                TRACE("solve_eqs_bug2", tout << "eliminating: " << mk_ismt2_pp(f, m()) << "\n";);
-                return true;
-            }
-            
-            if (is_neg_literal(f)) {
-                var = to_app(to_app(f)->get_arg(0));
-                if (m_candidate_vars.is_marked(var))
-                    return false;
-                def = m().mk_false();
-                if (m_produce_proofs) {
-                    // [rewrite]: (iff (iff l false) ~l)
-                    // [symmetry T1]: (iff ~l (iff l false))
-                    pr = m().mk_rewrite(m().mk_eq(var, def), f);
-                    pr = m().mk_symmetry(pr);
-                }
-                return true;
-            }
-            
-            return false;
-        }
-
-        void insert_solution(goal const& g, unsigned idx, expr* f, app* var, expr* def, proof* pr) {
-
-            if (!is_safe(var))
-                return;
-            m_vars.push_back(var);
-            m_candidates.push_back(f);
-            m_candidate_set.mark(f);
-            m_candidate_vars.mark(var);
-            m_marked_candidates.push_back(f);
-            if (m_produce_proofs) {
-                if (!pr)
-                    pr = g.pr(idx);
-                else
-                    pr = m().mk_modus_ponens(g.pr(idx), pr);
-            }
-            IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(var, m()) << " -> " << mk_bounded_pp(def, m()) << "\n");
-            m_subst->insert(var, def, pr, g.dep(idx));
-        }
-        
-        /**
-           \brief Start collecting candidates
-        */
-        void collect(goal const & g) {
-            m_subst->reset();
-            m_norm_subst->reset();
-            m_r->set_substitution(nullptr);
-            m_candidate_vars.reset();
-            m_candidate_set.reset();
-            m_candidates.reset();
-            m_marked_candidates.reset();
-            m_vars.reset();
-            m_nonzero.reset();
-            app_ref  var(m());
-            expr_ref  def(m());
-            proof_ref pr(m());
-            unsigned size = g.size();
-            for (unsigned idx = 0; idx < size; idx++) {
-                add_pos(g.form(idx));
-            }
-            for (unsigned idx = 0; idx < size; idx++) {
-                checkpoint();
-                expr * f = g.form(idx);
-                pr = nullptr;
-                if (solve(f, var, def, pr)) {
-                    insert_solution(g, idx, f, var, def, pr);
-                }
-                m_num_steps++;
-            }
-            
-            TRACE("solve_eqs", 
-                  tout << "candidate vars:\n";
-                  for (app* v : m_vars) {
-                      tout << mk_ismt2_pp(v, m()) << " ";
-                  }
-                  tout << "\n";);
-        }
-
-        struct nnf_context {
-            bool m_is_and;
-            expr_ref_vector m_args;
-            unsigned m_index;
-            nnf_context(bool is_and, expr_ref_vector const& args, unsigned idx):
-                m_is_and(is_and),
-                m_args(args),
-                m_index(idx)
-            {}
-        };
-
-        ptr_vector<expr> m_todo;       
-        void mark_occurs(expr_mark& occ, goal const& g, expr* v) {
-            SASSERT(m_todo.empty());
-            for (unsigned j = 0; j < g.size(); ++j)             
-                m_todo.push_back(g.form(j));            
-            ::mark_occurs(m_todo, v, occ);
-            SASSERT(m_todo.empty());
-        }
-
-        expr_mark m_compatible_tried;
-        expr_ref_vector m_var_trail;
-
-        bool is_compatible(goal const& g, unsigned idx, vector<nnf_context> const & path, expr* v, expr* eq) {
-            if (m_compatible_tried.is_marked(v))
-                return false;
-            m_compatible_tried.mark(v);
-            m_var_trail.push_back(v);
-            expr_mark occ;
-            svector<lbool> cache;
-            mark_occurs(occ, g, v);
-            return is_goal_compatible(g, occ, cache, idx, v, eq) && is_path_compatible(occ, cache, path, v, eq);
-        }
-
-        bool is_goal_compatible(goal const& g, expr_mark& occ, svector<lbool>& cache, unsigned idx, expr* v, expr* eq) {
-            bool all_e = false;
-            for (unsigned j = 0; j < g.size(); ++j) {              
-                if (j != idx && !check_eq_compat_rec(occ, cache, g.form(j), v, eq, all_e)) {
-                    TRACE("solve_eqs", tout << "occurs goal " << mk_pp(eq, m()) << "\n";);
-                    return false;
-                }
-            }
-            return true;
-        }
-
-        // 
-        // all_e := all disjunctions contain eq
-        //
-        // or, all_e -> skip if all disjunctions contain eq
-        // or, all_e -> fail if some disjunction contains v but not eq
-        // or, all_e -> all_e := false if some disjunction does not contain v
-        // and, all_e -> all_e
-        //
-
-        bool is_path_compatible(expr_mark& occ, svector<lbool>& cache, vector<nnf_context> const & path, expr* v, expr* eq) {
-            bool all_e = true;
-            auto is_marked = [&](expr* e) {
-                if (occ.is_marked(e))
-                    return true;
-                if (m().is_not(e, e) && occ.is_marked(e))
-                    return true;
-                return false;
-            };
-            for (unsigned i = path.size(); i-- > 0; ) {
-                auto const& p = path[i];
-                auto const& args = p.m_args;
-                if (p.m_is_and && !all_e) {
-                    for (unsigned j = 0; j < args.size(); ++j) {
-                        if (j != p.m_index && is_marked(args[j])) {
-                            TRACE("solve_eqs", tout << "occurs and " << mk_pp(eq, m()) << " " << mk_pp(args[j], m()) << "\n";);
-                            return false;
-                        }
-                    }
-                }
-                else if (!p.m_is_and) {
-                    for (unsigned j = 0; j < args.size(); ++j) {
-                        if (j != p.m_index) {
-                            if (occurs(v, args[j])) {
-                                if (!check_eq_compat_rec(occ, cache, args[j], v, eq, all_e)) {
-                                    TRACE("solve_eqs", tout << "occurs or " << mk_pp(eq, m()) << " " << mk_pp(args[j], m()) << "\n";);
-                                    return false;
-                                }
-                            }
-                            else {
-                                all_e = false;
-                            }
-                        }
-                    }
-                }
-            }
-            return true;
-        }
-
-        bool check_eq_compat_rec(expr_mark& occ, svector<lbool>& cache, expr* f, expr* v, expr* eq, bool& all) {
-            expr_ref_vector args(m());
-            expr* f1 = nullptr;
-            // flattening may introduce fresh negations, 
-            // occ is not defined on these negations
-            if (!m().is_not(f) && !occ.is_marked(f)) {
-                all = false;
-                return true;
-            }
-            unsigned idx = f->get_id();
-            if (cache.size() > idx && cache[idx] != l_undef) {
-                return cache[idx] == l_true;
-            }
-            if (m().is_not(f, f1) && m().is_or(f1)) {
-                flatten_and(f, args);
-                for (expr* arg : args) {
-                    if (arg == eq) {
-                        cache.reserve(idx+1, l_undef);
-                        cache[idx] = l_true;
-                        return true;
-                    }
-                }                
-            }
-            else if (m().is_or(f)) {
-                flatten_or(f, args);
-            }
-            else {
-                return false;
-            }
-
-            for (expr* arg : args) {
-                if (!check_eq_compat_rec(occ, cache, arg, v, eq, all)) {
-                    cache.reserve(idx+1, l_undef);
-                    cache[idx] = l_false;
-                    return false;
-                }
-            }
-            cache.reserve(idx+1, l_undef);
-            cache[idx] = l_true;
-            return true;
-        }
-
-        void hoist_nnf(goal const& g, expr* f, vector<nnf_context> & path, unsigned idx, unsigned depth, ast_mark& mark) {
-            if (depth > 3 || mark.is_marked(f)) {
-                return;
-            }
-            mark.mark(f, true);
-            checkpoint();
-            app_ref var(m());
-            expr_ref def(m());
-            proof_ref pr(m());
-            expr_ref_vector args(m());
-            expr* f1 = nullptr;
-
-            if (m().is_not(f, f1) && m().is_or(f1)) {
-                flatten_and(f, args);
-                for (unsigned i = 0; i < args.size(); ++i) {
-                    pr = nullptr;
-                    expr* arg = args.get(i), *lhs = nullptr, *rhs = nullptr;
-                    if (m().is_eq(arg, lhs, rhs) && !m().is_bool(lhs)) {                
-                        if (trivial_solve1(lhs, rhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) {
-                            IF_VERBOSE(11, verbose_stream() << "nested " << mk_bounded_pp(var.get(), m()) << " -> " << mk_bounded_pp(def, m()) << "\n");
-                            insert_solution(g, idx, arg, var, def, pr);
-                        }
-                        else if (trivial_solve1(rhs, lhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) {
-                            IF_VERBOSE(11, verbose_stream() << "nested " << mk_bounded_pp(var.get(), m()) << " -> " << mk_bounded_pp(def, m()) << "\n");
-                            insert_solution(g, idx, arg, var, def, pr);
-                        }
-                        else {
-                            IF_VERBOSE(10000, 
-                                       verbose_stream() << "eq not solved " << mk_pp(arg, m()) << "\n";
-                                       verbose_stream() << is_uninterp_const(lhs) << " " << !m_candidate_vars.is_marked(lhs) << " " 
-                                       << !occurs(lhs, rhs) << " " << check_occs(lhs) << "\n";);
-                        }
-                    }
-                    else {
-                        path.push_back(nnf_context(true, args, i));
-                        hoist_nnf(g, arg, path, idx, depth + 1, mark);
-                        path.pop_back();
-                    }                             
-                }
-            }
-            else if (m().is_or(f)) {
-                flatten_or(f, args);
-                for (unsigned i = 0; i < args.size(); ++i) {
-                    path.push_back(nnf_context(false, args, i));
-                    hoist_nnf(g, args.get(i), path, idx, depth + 1, mark);
-                    path.pop_back();
-                }
-            }
-        }
-
-        void collect_hoist(goal const& g) {
-            unsigned size = g.size();
-            ast_mark mark;
-            vector<nnf_context> path;
-            for (unsigned idx = 0; idx < size; idx++) {
-                checkpoint();
-                hoist_nnf(g, g.form(idx), path, idx, 0, mark);
-            }
-        }
-
-        void distribute_and_or(goal & g) {
-            if (m_produce_proofs) 
-                return;
-            unsigned size = g.size();
-            hoist_rewriter_star rw(m(), m_params);
-            th_rewriter thrw(m(), m_params);
-            expr_ref tmp(m()), tmp2(m());
-            
-            TRACE("solve_eqs", g.display(tout););
-            for (unsigned idx = 0; !g.inconsistent() && idx < size; idx++) {
-                checkpoint();
-                if (g.is_decided_unsat()) break;
-                expr* f = g.form(idx);
-                proof_ref pr1(m()), pr2(m());
-                thrw(f, tmp, pr1);
-                rw(tmp, tmp2, pr2);
-                TRACE("solve_eqs", tout << mk_pp(f, m()) << "\n->\n" << tmp << "\n->\n" << tmp2 
-                      << "\n" << pr1 << "\n" << pr2 << "\n" << mk_pp(g.pr(idx), m()) << "\n";);
-                pr1 = m().mk_transitivity(pr1, pr2);
-                if (!pr1) pr1 = g.pr(idx); else pr1 = m().mk_modus_ponens(g.pr(idx), pr1);
-                g.update(idx, tmp2, pr1, g.dep(idx));
-            }            
-        }
-
-        expr_mark m_unsafe_vars;        
-
-        void filter_unsafe_vars() {
-            m_unsafe_vars.reset();
-            recfun::util rec(m());
-            for (func_decl* f : rec.get_rec_funs()) 
-                for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m())))
-                    m_unsafe_vars.mark(term);            
-        }
-
-        bool is_safe(expr* f) {
-            return !m_unsafe_vars.is_marked(f);
-        }
-        
-        void sort_vars() {
-            SASSERT(m_candidates.size() == m_vars.size());
-            TRACE("solve_eqs_bug", tout << "sorting vars...\n";);
-            m_ordered_vars.reset();
-            
-
-            // The variables (and its definitions) in m_subst must remain alive until the end of this procedure.
-            // Reason: they are scheduled for unmarking in visiting/done. 
-            // They should remain alive while they are on the stack.
-            // To make sure this is the case, whenever a variable (and its definition) is removed from m_subst,
-            // I add them to the saved vector. 
-            
-            expr_ref_vector saved(m());
-            
-            expr_fast_mark1 visiting;
-            expr_fast_mark2 done;
-            
-            typedef std::pair<expr *, unsigned> frame;
-            svector<frame> todo;
-            unsigned num = 0;
-            for (app* v : m_vars) {
-                checkpoint();
-                if (!m_candidate_vars.is_marked(v))
-                    continue;
-                todo.push_back(frame(v, 0));
-                while (!todo.empty()) {
-                start:
-                    frame & fr = todo.back();
-                    expr * t   = fr.first;
-                    m_num_steps++;
-                    TRACE("solve_eqs_bug", tout << "processing:\n" << mk_ismt2_pp(t, m()) << "\n";);
-                    if (t->get_ref_count() > 1 && done.is_marked(t)) {
-                        todo.pop_back();
-                        continue;
-                    }
-                    switch (t->get_kind()) {
-                    case AST_VAR:
-                        todo.pop_back();
-                        break;
-                    case AST_QUANTIFIER:
-                        num = to_quantifier(t)->get_num_children();
-                        while (fr.second < num) {
-                            expr * c = to_quantifier(t)->get_child(fr.second);
-                            fr.second++;
-                            if (c->get_ref_count() > 1 && done.is_marked(c))
-                                continue;
-                            todo.push_back(frame(c, 0));
-                            goto start;
-                        }
-                        if (t->get_ref_count() > 1)
-                            done.mark(t);
-                        todo.pop_back();
-                        break;
-                    case AST_APP:
-                        num = to_app(t)->get_num_args();
-                        if (num == 0) {
-                            if (fr.second == 0) {
-                                if (m_candidate_vars.is_marked(t)) {
-                                    if (visiting.is_marked(t)) {
-                                        // cycle detected: remove t
-                                        visiting.reset_mark(t);
-                                        m_candidate_vars.mark(t, false);
-                                        SASSERT(!m_candidate_vars.is_marked(t));
-                                        
-                                        // Must save t and its definition.
-                                        // See comment in the beginning of the function
-                                        expr * def = nullptr;
-                                        proof * pr;
-                                        expr_dependency * dep;
-                                        m_subst->find(to_app(t), def, pr, dep);
-                                        SASSERT(def != 0);
-                                        saved.push_back(t); 
-                                        saved.push_back(def);
-                                        // 
-                                        
-                                        m_subst->erase(t);
-                                    }
-                                    else {
-                                        visiting.mark(t);
-                                        fr.second = 1;
-                                        expr * def = nullptr;
-                                        proof * pr;
-                                        expr_dependency * dep;
-                                        m_subst->find(to_app(t), def, pr, dep);
-                                        SASSERT(def != 0);
-                                        todo.push_back(frame(def, 0));
-                                        goto start;
-                                    }
-                                }
-                            }
-                            else {
-                                SASSERT(fr.second == 1);
-                                if (m_candidate_vars.is_marked(t)) {
-                                    visiting.reset_mark(t);
-                                    m_ordered_vars.push_back(to_app(t));
-                                }
-                                else {
-                                    // var was removed from the list of candidate vars to elim cycle
-                                    // do nothing
-                                }
-                            }
-                        }
-                        else {
-                            while (fr.second < num) {
-                                expr * arg = to_app(t)->get_arg(fr.second);
-                                fr.second++;
-                                if (arg->get_ref_count() > 1 && done.is_marked(arg))
-                                    continue;
-                                todo.push_back(frame(arg, 0));
-                                goto start;
-                            }
-                        }
-                        if (t->get_ref_count() > 1)
-                            done.mark(t);
-                        todo.pop_back();
-                        break;
-                    default:
-                        UNREACHABLE();
-                        todo.pop_back();
-                        break;
-                    }
-                }
-            }
-            
-            // cleanup
-            unsigned idx = 0;
-            for (expr* v : m_vars) {
-                if (!m_candidate_vars.is_marked(v)) {
-                    m_candidate_set.mark(m_candidates[idx], false);
-                    m_marked_candidates.push_back(m_candidates[idx]);
-                    m_marked_candidates.push_back(v);
-                }
-                ++idx;
-            }
-            
-            IF_VERBOSE(10000, 
-                       verbose_stream() << "ordered vars: ";
-                       for (app* v : m_ordered_vars) verbose_stream() << mk_pp(v, m()) << " ";
-                       verbose_stream() << "\n";);
-            TRACE("solve_eqs", 
-                  tout << "ordered vars:\n";
-                  for (app* v : m_ordered_vars) {
-                      SASSERT(m_candidate_vars.is_marked(v));
-                      tout << mk_ismt2_pp(v, m()) << " ";
-                  }
-                  tout << "\n";);
-            m_candidate_vars.reset();
-        }
-        
-        void normalize() {
-            m_norm_subst->reset();
-            m_r->set_substitution(m_norm_subst.get());
-            
-
-            expr_dependency_ref new_dep(m());
-            for (app * v : m_ordered_vars) {
-                checkpoint();
-                expr_ref new_def(m());
-                proof_ref new_pr(m());
-                expr * def = nullptr;
-                proof * pr = nullptr;
-                expr_dependency * dep = nullptr;
-                m_subst->find(v, def, pr, dep);
-                SASSERT(def);
-                m_r->operator()(def, new_def, new_pr, new_dep);
-                m_num_steps += m_r->get_num_steps() + 1;
-                if (m_produce_proofs)
-                    new_pr = m().mk_transitivity(pr, new_pr);
-                new_dep = m().mk_join(dep, new_dep);
-                m_norm_subst->insert(v, new_def, new_pr, new_dep);
-                // we updated the substituting, but we don't need to reset m_r
-                // because all cached values there do not depend on v.
-            }
-            m_subst->reset();
-            TRACE("solve_eqs", 
-                  tout << "after normalizing variables\n";
-                  for (expr * v : m_ordered_vars) {
-                      expr * def = 0;
-                      proof * pr = 0;
-                      expr_dependency * dep = 0;
-                      m_norm_subst->find(v, def, pr, dep);
-                      tout << mk_ismt2_pp(v, m()) << "\n----->\n" << mk_ismt2_pp(def, m()) << "\n\n";
-                  });
-        }
-
-        void substitute(goal & g) {
-            // force the cache of m_r to be reset.
-            m_r->set_substitution(m_norm_subst.get());
-            
-            expr_ref new_f(m());
-            proof_ref new_pr(m());
-            expr_dependency_ref new_dep(m());
-            unsigned size = g.size();
-            for (unsigned idx = 0; idx < size; idx++) {
-                checkpoint();
-                expr * f = g.form(idx);
-                TRACE("gaussian_leak", tout << "processing:\n" << mk_ismt2_pp(f, m()) << "\n";);
-                if (m_candidate_set.is_marked(f)) {
-                    m_marked_candidates.push_back(f);
-                    // f may be deleted after the following update.
-                    // so, we must remove the mark before doing the update
-                    m_candidate_set.mark(f, false);
-                    SASSERT(!m_candidate_set.is_marked(f));
-                    g.update(idx, m().mk_true(), m().mk_true_proof(), nullptr);
-                    m_num_steps ++;
-                    continue;
-                }
-
-                m_r->operator()(f, new_f, new_pr, new_dep);
-
-                TRACE("solve_eqs_subst", tout << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n";);
-                m_num_steps += m_r->get_num_steps() + 1;
-                if (m_produce_proofs)
-                    new_pr = m().mk_modus_ponens(g.pr(idx), new_pr);
-                if (m_produce_unsat_cores)
-                    new_dep = m().mk_join(g.dep(idx), new_dep);
-                
-                g.update(idx, new_f, new_pr, new_dep);
-                if (g.inconsistent())
-                    return;
-            }
-            g.elim_true();
-            TRACE("solve_eqs", g.display(tout << "after applying substitution\n"););
-#if 0
-            DEBUG_CODE({
-                    for (expr* v : m_ordered_vars) {
-                        for (unsigned j = 0; j < g.size(); j++) {
-                            CASSERT("solve_eqs_bug", !occurs(v, g.form(j)));
-                        }
-                    }});
-#endif
-        }
-
-        void save_elim_vars(model_converter_ref & mc) {
-            IF_VERBOSE(100, if (!m_ordered_vars.empty()) verbose_stream() << "num. eliminated vars: " << m_ordered_vars.size() << "\n";);
-            m_num_eliminated_vars += m_ordered_vars.size();
-            if (m_produce_models) {
-                if (!mc.get())
-                    mc = alloc(gmc, m(), "solve-eqs");
-                for (app* v : m_ordered_vars) 
-                    static_cast<gmc*>(mc.get())->add(v, m_norm_subst->find(v));
-            }
-        }
-        
-        void collect_num_occs(expr * t, expr_fast_mark1 & visited) {
-            ptr_buffer<app, 128> stack;
-            
-            auto visit = [&](expr* arg) {
-                if (is_uninterp_const(arg)) {                           
-                    m_num_occs.insert_if_not_there(arg, 0)++;           
-                }                                                       
-                if (!visited.is_marked(arg) && is_app(arg)) {                          
-                    visited.mark(arg, true);                            
-                    stack.push_back(to_app(arg));                               
-                }                                                       
-            };
-            
-            visit(t);
-            
-            while (!stack.empty()) {
-                app * t = stack.back();
-                stack.pop_back();
-                for (expr* arg : *t) 
-                    visit(arg);
-            }
-        }
-        
-        void collect_num_occs(goal const & g) {
-            if (m_max_occs == UINT_MAX)
-                return; // no need to compute num occs
-            m_num_occs.reset();
-            expr_fast_mark1 visited;
-            unsigned sz = g.size();
-            for (unsigned i = 0; i < sz; i++)
-                collect_num_occs(g.form(i), visited);
-        }
-        
-        unsigned get_num_steps() const {
-            return m_num_steps;
-        }
-        
-        unsigned get_num_eliminated_vars() const {
-            return m_num_eliminated_vars;
-        }
-
-        void collect_statistics(statistics& st) {
-            st.update("solve eqs elim vars", get_num_eliminated_vars());
-        }
-        
-        //
-        // TBD: rewrite the tactic to first apply a topological sorting that
-        // approximates the dependencies between variables. Then apply 
-        // simplification on top of this sorting, so that it can apply sub-quadratic
-        // equality and unit propagation.
-        //
-        void operator()(goal_ref const & g, goal_ref_buffer & result) {
-            model_converter_ref mc;
-            std::function<void(statistics&)> coll = [&](statistics& st) { collect_statistics(st); };
-            statistics_report sreport(coll);
-            tactic_report report("solve_eqs", *g);
-            TRACE("goal", g->display(tout););
-            m_produce_models = g->models_enabled();
-            m_produce_proofs = g->proofs_enabled();
-            m_produce_unsat_cores = g->unsat_core_enabled();
-
-            if (!g->inconsistent()) {
-                m_subst      = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs);
-                m_norm_subst = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs);
-                unsigned rounds = 0;
-
-                filter_unsafe_vars();
-                while (rounds < 20) {
-                    ++rounds;
-                    if (!m_produce_proofs && m_context_solve && rounds < 3) {
-                        distribute_and_or(*(g.get()));
-                    }
-                    collect_num_occs(*g);
-                    collect(*g);
-                    if (!m_produce_proofs && m_context_solve && rounds < 3) {
-                        collect_hoist(*g);
-                    }
-                    if (m_subst->empty()) {
-                        break;
-                    }
-                    sort_vars();
-                    if (m_ordered_vars.empty()) {
-                        break;
-                    }
-                    normalize();
-                    substitute(*(g.get()));
-                    if (g->inconsistent()) {
-                        break;
-                    }
-                    save_elim_vars(mc);
-                    TRACE("solve_eqs_round", g->display(tout); if (mc) mc->display(tout););
-                    if (rounds > 10 && m_ordered_vars.size() == 1)
-                        break;
-                }
-            }
-            g->inc_depth();
-            g->add(mc.get());
-            result.push_back(g.get());
-
-            
-        }
-    };
-    
-    imp *      m_imp;
-public:
-    solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r, bool owner) {
-        m_imp = alloc(imp, m, p, r, owner);
-    }
-
-    tactic * translate(ast_manager & m) override {
-        return alloc(solve_eqs_tactic, m, m_imp->m_params, mk_expr_simp_replacer(m, m_imp->m_params), true);
-    }
-        
-    ~solve_eqs_tactic() override {
-        dealloc(m_imp);
-    }
-
-    char const* name() const override { return "solve_eqs"; }
-
-    void updt_params(params_ref const & p) override {
-        m_imp->updt_params(p);
-    }
-
-    void collect_param_descrs(param_descrs & r) override {        
-        r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.");
-        r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers.");
-        r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver.");
-        r.insert("context_solve", CPK_BOOL, "(default: false) solve equalities under disjunctions.");
-    }
-    
-    void operator()(goal_ref const & in, 
-                    goal_ref_buffer & result) override {
-        (*m_imp)(in, result);
-    }
-    
-    void cleanup() override {
-        unsigned num_elim_vars = m_imp->m_num_eliminated_vars;
-        ast_manager & m = m_imp->m();
-        expr_replacer * r = m_imp->m_r;
-        if (r)
-            r->set_substitution(nullptr);
-        bool owner = m_imp->m_r_owner;
-        m_imp->m_r_owner  = false; // stole replacer
-
-        imp * d = alloc(imp, m, m_imp->m_params, r, owner);
-        d->m_num_eliminated_vars = num_elim_vars;
-        std::swap(d, m_imp);        
-        dealloc(d);
-    }
-
-    void collect_statistics(statistics & st) const override {
-        m_imp->collect_statistics(st);        
-    }
-
-    void reset_statistics() override {
-        m_imp->m_num_eliminated_vars = 0;
-    }
-    
-};
-
-tactic * mk_solve_eqs1_tactic(ast_manager & m, params_ref const & p) {
-    return clean(alloc(solve_eqs_tactic, m, p, mk_expr_simp_replacer(m, p), true));
-}
diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h
index 7b97172a3..fa095aad0 100644
--- a/src/tactic/core/solve_eqs_tactic.h
+++ b/src/tactic/core/solve_eqs_tactic.h
@@ -1,37 +1,47 @@
 /*++
-Copyright (c) 2011 Microsoft Corporation
+Copyright (c) 2022 Microsoft Corporation
 
 Module Name:
 
-    solve_eqs_tactic.h
+    solve_eqs2_tactic.h
 
 Abstract:
 
-    Tactic for solving equations and performing gaussian elimination.
+    Tactic for solving variables
 
 Author:
 
-    Leonardo de Moura (leonardo) 2011-12-29.
-
-Revision History:
+    Nikolaj Bjorner (nbjorner) 2022-10-30
 
 --*/
 #pragma once
 
 #include "util/params.h"
-class ast_manager;
-class tactic;
+#include "tactic/tactic.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/solve_eqs.h"
 
-tactic * mk_solve_eqs1_tactic(ast_manager & m, params_ref const & p = params_ref());
 
-#if 0
+class solve_eqs2_tactic_factory : public dependent_expr_simplifier_factory {
+public:
+    dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override {
+        return alloc(euf::solve_eqs, m, s);
+    }
+};
+
+inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs");
+}
+
+#if 1
 inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
-    return mk_solve_eqs1_tactic(m, p);
+    return mk_solve_eqs2_tactic(m, p);
 }
 #endif
 
+
 /*
-  ADD_TACTIC("solve-eqs", "eliminate variables by solving equations.", "mk_solve_eqs1_tactic(m, p)")
+  ADD_TACTIC("solve-eqs", "solve for variables.", "mk_solve_eqs2_tactic(m, p)")
 */
 
 
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
index 419037839..aaf744d5f 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/src/tactic/dependent_expr_state_tactic.h
@@ -81,6 +81,11 @@ public:
         m_simp->updt_params(m_params);
     }
 
+    void collect_param_descrs(param_descrs& r) override {
+        init();
+        m_simp->collect_param_descrs(r);
+    }
+
     tactic * translate(ast_manager & m) override {
         return alloc(dependent_expr_state_tactic, m, m_params, m_factory.get(), name());
     }
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index a09da60a9..e631c23e9 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -18,7 +18,6 @@ Notes:
 --*/
 #include "ast/normal_forms/nnf.h"
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/bv/bv_size_reduction_tactic.h"
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "tactic/core/simplify_tactic.h"
diff --git a/src/tactic/smtlogics/qfaufbv_tactic.cpp b/src/tactic/smtlogics/qfaufbv_tactic.cpp
index 6d44addf0..acad15fd6 100644
--- a/src/tactic/smtlogics/qfaufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfaufbv_tactic.cpp
@@ -17,7 +17,6 @@ Notes:
 
 --*/
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/bv/bit_blaster_tactic.h"
diff --git a/src/tactic/smtlogics/qfauflia_tactic.cpp b/src/tactic/smtlogics/qfauflia_tactic.cpp
index 9ca6b70ef..2f1879d58 100644
--- a/src/tactic/smtlogics/qfauflia_tactic.cpp
+++ b/src/tactic/smtlogics/qfauflia_tactic.cpp
@@ -21,7 +21,6 @@ Notes:
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/smtlogics/smt_tactic.h"
 
diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index 90df4fe42..07784eb3b 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -20,7 +20,6 @@ Notes:
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/bv/bit_blaster_tactic.h"
 #include "tactic/bv/bv1_blaster_tactic.h"
diff --git a/src/tactic/smtlogics/qfidl_tactic.cpp b/src/tactic/smtlogics/qfidl_tactic.cpp
index 5c1ba5f44..c86789ed0 100644
--- a/src/tactic/smtlogics/qfidl_tactic.cpp
+++ b/src/tactic/smtlogics/qfidl_tactic.cpp
@@ -21,7 +21,6 @@ Notes:
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/arith/normalize_bounds_tactic.h"
 #include "tactic/arith/fix_dl_var_tactic.h"
diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp
index d116414ea..b8ebbd8a9 100644
--- a/src/tactic/smtlogics/qflia_tactic.cpp
+++ b/src/tactic/smtlogics/qflia_tactic.cpp
@@ -22,7 +22,6 @@ Notes:
 #include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/arith/normalize_bounds_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/arith/add_bounds_tactic.h"
 #include "tactic/arith/pb2bv_tactic.h"
diff --git a/src/tactic/smtlogics/qfuf_tactic.cpp b/src/tactic/smtlogics/qfuf_tactic.cpp
index d9f723d67..609107a48 100644
--- a/src/tactic/smtlogics/qfuf_tactic.cpp
+++ b/src/tactic/smtlogics/qfuf_tactic.cpp
@@ -21,7 +21,6 @@ Notes:
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/symmetry_reduce_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/smtlogics/smt_tactic.h"
 
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index 98e09b56a..6ba3e8cc9 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -21,7 +21,6 @@ Notes:
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "tactic/bv/bv_size_reduction_tactic.h"
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index 3bf6b658d..daf020a14 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -20,7 +20,6 @@ Revision History:
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "qe/lite/qe_lite.h"
 #include "qe/qsat.h"
diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp
index 728e6397d..e8495c013 100644
--- a/src/tactic/ufbv/ufbv_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_tactic.cpp
@@ -20,7 +20,6 @@ Notes:
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
-#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/distribute_forall_tactic.h"
 #include "tactic/core/der_tactic.h"
 #include "tactic/core/reduce_args_tactic.h"