diff --git a/CMakeLists.txt b/CMakeLists.txt
index d79a01da71f..78929fed61d 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -2,7 +2,7 @@
 cmake_minimum_required(VERSION 3.4)
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.12.0.0 LANGUAGES CXX)
+project(Z3 VERSION 4.12.1.0 LANGUAGES CXX)
 
 ################################################################################
 # Project version
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index a16913317f3..3e7386601d5 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -8,7 +8,7 @@
 from mk_util import *
 
 def init_version():
-    set_version(4, 12, 0, 0) # express a default build version or pick up ci build version
+    set_version(4, 12, 1, 0) # express a default build version or pick up ci build version
     
 # Z3 Project definition
 def init_project_def():
diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml
index c93738e58c2..4e602797610 100644
--- a/scripts/nightly.yaml
+++ b/scripts/nightly.yaml
@@ -1,7 +1,7 @@
 variables:
   Major: '4'
   Minor: '12'
-  Patch: '0'
+  Patch: '1'
   AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
   NightlyVersion: $(AssemblyVersion)-$(Build.DefinitionName)
 
diff --git a/scripts/release.yml b/scripts/release.yml
index 4421f515386..42a5bbcc6c0 100644
--- a/scripts/release.yml
+++ b/scripts/release.yml
@@ -6,7 +6,7 @@
 trigger: none
 
 variables:
-  ReleaseVersion: '4.12.0'
+  ReleaseVersion: '4.12.1'
 
 stages:
 
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index ad88f839fc8..115a3f53f6f 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -91,9 +91,7 @@ namespace euf {
             m_scopes.push_back(m_updates.size());
             m_region.push_scope();
             m_updates.push_back(update_record(m_new_th_eqs_qhead, update_record::new_th_eq_qhead()));
-            m_updates.push_back(update_record(m_new_lits_qhead, update_record::new_lits_qhead()));
         }
-        SASSERT(m_new_lits_qhead <= m_new_lits.size());
         SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size());
     }
 
@@ -156,12 +154,29 @@ namespace euf {
     }
 
     void egraph::add_literal(enode* n, enode* ante) {
+        /*
         if (n->bool_var() == sat::null_bool_var)
             return;
-        TRACE("euf_verbose", tout << "lit: " << n->get_expr_id() << "\n";);
-        m_new_lits.push_back(enode_pair(n, ante));
-        m_updates.push_back(update_record(update_record::new_lit()));
+        */
         if (!ante) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits;
+        if (!ante)
+            m_on_propagate_literal(n, ante);
+        else if (m.is_true(ante->get_expr()) || m.is_false(ante->get_expr())) {
+            for (enode* k : enode_class(n)) {
+                if (k != ante) {
+                    //verbose_stream() << "eq: " << k->value() << " " <<ante->value() << "\n";
+                    m_on_propagate_literal(k, ante);
+                }
+            }
+        }
+        else {
+            for (enode* k : enode_class(n)) {
+                if (k->value() != ante->value()) {
+                    //verbose_stream() << "eq: " << k->value() << " " <<ante->value() << "\n";
+                    m_on_propagate_literal(k, ante);
+                }
+            }
+        }
     }
 
     void egraph::new_diseq(enode* n) {
@@ -339,7 +354,6 @@ namespace euf {
         num_scopes -= m_num_scopes;
         m_num_scopes = 0;
 
-        SASSERT(m_new_lits_qhead <= m_new_lits.size());
         unsigned old_lim = m_scopes.size() - num_scopes;
         unsigned num_updates = m_scopes[old_lim];
         auto undo_node = [&]() {
@@ -378,18 +392,12 @@ namespace euf {
                 SASSERT(p.r1->get_th_var(p.m_th_id) != null_theory_var);
                 p.r1->replace_th_var(p.m_old_th_var, p.m_th_id);
                 break;
-            case update_record::tag_t::is_new_lit:
-                m_new_lits.pop_back();
-                break;
             case update_record::tag_t::is_new_th_eq:
                 m_new_th_eqs.pop_back();
                 break;
             case update_record::tag_t::is_new_th_eq_qhead:
                 m_new_th_eqs_qhead = p.qhead;
                 break;
-            case update_record::tag_t::is_new_lits_qhead:
-                m_new_lits_qhead = p.qhead;
-                break;
             case update_record::tag_t::is_inconsistent:
                 m_inconsistent = p.m_inconsistent;
                 break;
@@ -424,7 +432,6 @@ namespace euf {
         m_region.pop_scope(num_scopes);  
         m_to_merge.reset();
 
-        SASSERT(m_new_lits_qhead <= m_new_lits.size());
         SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size());
 
         // DEBUG_CODE(invariant(););
@@ -461,12 +468,6 @@ namespace euf {
             std::swap(n1, n2);
         }
 
-        if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr())))
-            add_literal(n1, r2);
-        if (r2->value() != l_undef && n1->value() == l_undef) 
-            add_literal(n1, r2);
-        else if (r1->value() != l_undef && n2->value() == l_undef) 
-            add_literal(n2, r1);
         remove_parents(r1);
         push_eq(r1, n1, r2->num_parents());
         merge_justification(n1, n2, j);
@@ -476,6 +477,13 @@ namespace euf {
         r2->inc_class_size(r1->class_size());   
         merge_th_eq(r1, r2);
         reinsert_parents(r1, r2);
+        if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr())))
+            add_literal(n1, r2);
+        else if (n2->value() != l_undef && n1->value() != n2->value()) 
+            add_literal(n1, n2);
+        else if (n1->value() != l_undef && n2->value() != n1->value()) 
+            add_literal(n2, n1);
+
         for (auto& cb : m_on_merge)
             cb(r2, r1);
     }
@@ -565,7 +573,6 @@ namespace euf {
 
 
     bool egraph::propagate() {
-        SASSERT(m_new_lits_qhead <= m_new_lits.size());
         SASSERT(m_num_scopes == 0 || m_to_merge.empty());
         force_push();
         for (unsigned i = 0; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) {
@@ -574,7 +581,6 @@ namespace euf {
         }
         m_to_merge.reset();
         return 
-            (m_new_lits_qhead < m_new_lits.size()) || 
             (m_new_th_eqs_qhead < m_new_th_eqs.size()) ||
             inconsistent();
     }
@@ -851,7 +857,6 @@ namespace euf {
 
     std::ostream& egraph::display(std::ostream& out) const {
         out << "updates " << m_updates.size() << "\n";
-        out << "newlits " << m_new_lits.size()   << " qhead: " << m_new_lits_qhead << "\n";
         out << "neweqs  " << m_new_th_eqs.size() << " qhead: " << m_new_th_eqs_qhead << "\n";
         m_table.display(out);
         unsigned max_args = 0;
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 1686be38469..c1b9b784953 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -105,10 +105,8 @@ namespace euf {
             struct toggle_merge_tf {};
             struct add_th_var {};
             struct replace_th_var {};
-            struct new_lit {};
             struct new_th_eq {};
             struct new_th_eq_qhead {};
-            struct new_lits_qhead {};
             struct inconsistent {};
             struct value_assignment {};
             struct lbl_hash {};
@@ -116,8 +114,8 @@ namespace euf {
             struct update_children {};
             struct set_relevant {};
             enum class tag_t { is_set_parent, is_add_node, is_toggle_cgc, is_toggle_merge_tf, is_update_children,
-                    is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq,
-                    is_lbl_hash, is_new_th_eq_qhead, is_new_lits_qhead, 
+                    is_add_th_var, is_replace_th_var, is_new_th_eq,
+                    is_lbl_hash, is_new_th_eq_qhead,
                     is_inconsistent, is_value_assignment, is_lbl_set, is_set_relevant };
             tag_t  tag;
             enode* r1;
@@ -145,14 +143,10 @@ namespace euf {
                 tag(tag_t::is_add_th_var), r1(n), n1(nullptr), r2_num_parents(id) {}
             update_record(enode* n, theory_id id, theory_var v, replace_th_var) :
                 tag(tag_t::is_replace_th_var), r1(n), n1(nullptr), m_th_id(id), m_old_th_var(v) {}
-            update_record(new_lit) :
-                tag(tag_t::is_new_lit), r1(nullptr), n1(nullptr), r2_num_parents(0) {}
             update_record(new_th_eq) :
                 tag(tag_t::is_new_th_eq), r1(nullptr), n1(nullptr), r2_num_parents(0) {}
             update_record(unsigned qh, new_th_eq_qhead):
                 tag(tag_t::is_new_th_eq_qhead), r1(nullptr), n1(nullptr), qhead(qh) {}
-            update_record(unsigned qh, new_lits_qhead):
-                tag(tag_t::is_new_lits_qhead), r1(nullptr), n1(nullptr), qhead(qh) {}
             update_record(bool inc, inconsistent) :
                 tag(tag_t::is_inconsistent), r1(nullptr), n1(nullptr), m_inconsistent(inc) {}
             update_record(enode* n, value_assignment) :
@@ -187,9 +181,7 @@ namespace euf {
         enode                  *m_n1 = nullptr;
         enode                  *m_n2 = nullptr;
         justification          m_justification;
-        unsigned               m_new_lits_qhead = 0;
         unsigned               m_new_th_eqs_qhead = 0;
-        svector<enode_pair>    m_new_lits;
         svector<th_eq>         m_new_th_eqs;
         bool_vector            m_th_propagates_diseqs;
         enode_vector           m_todo;
@@ -198,7 +190,8 @@ namespace euf {
         bool                   m_default_relevant = true;
         uint64_t               m_congruence_timestamp = 0;
 
-        std::vector<std::function<void(enode*,enode*)>>     m_on_merge;
+        std::vector<std::function<void(enode*,enode*)>> m_on_merge;
+        std::function<void(enode*, enode*)>    m_on_propagate_literal;
         std::function<void(enode*)>            m_on_make;
         std::function<void(expr*,expr*,expr*)> m_used_eq;
         std::function<void(app*,app*)>         m_used_cc;  
@@ -290,11 +283,8 @@ namespace euf {
            is an equality consequence. 
          */
         void       add_th_diseq(theory_id id, theory_var v1, theory_var v2, expr* eq);
-        bool       has_literal() const { return m_new_lits_qhead < m_new_lits.size(); }
         bool       has_th_eq() const { return m_new_th_eqs_qhead < m_new_th_eqs.size(); }
-        enode_pair get_literal() const { return m_new_lits[m_new_lits_qhead]; }
         th_eq      get_th_eq() const { return m_new_th_eqs[m_new_th_eqs_qhead]; }
-        void       next_literal() { force_push();  SASSERT(m_new_lits_qhead < m_new_lits.size()); m_new_lits_qhead++; }
         void       next_th_eq() { force_push(); SASSERT(m_new_th_eqs_qhead < m_new_th_eqs.size()); m_new_th_eqs_qhead++; }
 
         void set_lbl_hash(enode* n);
@@ -311,6 +301,7 @@ namespace euf {
         void set_default_relevant(bool b) { m_default_relevant = b; }
 
         void set_on_merge(std::function<void(enode* root,enode* other)>& on_merge) { m_on_merge.push_back(on_merge); }
+        void set_on_propagate(std::function<void(enode* lit,enode* ante)>& on_propagate) { m_on_propagate_literal = on_propagate; }
         void set_on_make(std::function<void(enode* n)>& on_make) { m_on_make = on_make; }
         void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; }
         void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; }
diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
index ef9263686c2..c3b5043a5a7 100644
--- a/src/ast/simplifiers/dependent_expr_state.h
+++ b/src/ast/simplifiers/dependent_expr_state.h
@@ -51,7 +51,6 @@ class dependent_expr_state {
     void freeze_recfun();
     void freeze_lambda();
     void freeze_terms(expr* term, bool only_as_array, ast_mark& visited);
-    void freeze(expr* term);
     void freeze(func_decl* f);
     struct thaw : public trail {
         unsigned sz;
@@ -89,6 +88,7 @@ class dependent_expr_state {
     /**
     * Freeze internal functions
     */
+    void freeze(expr* term);
     bool frozen(func_decl* f) const { return m_frozen.is_marked(f); }
     bool frozen(expr* f) const { return is_app(f) && m_frozen.is_marked(to_app(f)->get_decl()); }
     void freeze_suffix();
diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp
index 567546e67b1..e3cfc5c6fec 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.cpp
+++ b/src/ast/simplifiers/model_reconstruction_trail.cpp
@@ -23,11 +23,13 @@ Module Name:
 // substitutions that use variables from the dependent expressions.
 // TODO: add filters to skip sections of the trail that do not touch the current free variables.
 
-void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st) {
+void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumptions, dependent_expr_state& st) {
     ast_mark free_vars;
     scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
-    for (unsigned i = qhead; i < st.qtail(); ++i) 
+    for (unsigned i = qhead; i < st.qtail(); ++i)        
         add_vars(st[i], free_vars);
+    for (expr* a : assumptions)
+        add_vars(a, free_vars);
 
     for (auto& t : m_trail) {
         if (!t->m_active)
@@ -63,7 +65,7 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st
             mrp.insert(head, t->m_def, t->m_dep);
             dependent_expr de(m, t->m_def, nullptr, t->m_dep);
             add_vars(de, free_vars);
-
+            
             for (unsigned i = qhead; i < st.qtail(); ++i) {
                 auto [f, p, dep1] = st[i]();
                 expr_ref g(m);
@@ -73,6 +75,15 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st
                 if (f != g)
                     st.update(i, dependent_expr(m, g, nullptr, dep2));
             }
+            for (unsigned i = 0; i < assumptions.size(); ++i) {
+                expr* a = assumptions.get(i);
+                expr_ref g(m);
+                expr_dependency_ref dep(m);
+                mrp(a, nullptr, g, dep);
+                if (a != g)
+                    assumptions[i] = g;
+                // ignore dep.
+            }
             continue;
         }
 
@@ -103,7 +114,15 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st
             CTRACE("simplifier", f != g, tout << "updated " << mk_pp(g, m) << "\n");
             add_vars(d, free_vars);
             st.update(i, d);
-        }    
+        }
+        
+        for (unsigned i = 0; i < assumptions.size(); ++i) {
+            expr* a = assumptions.get(i);
+            auto [g, dep2] = rp->replace_with_dep(a);
+            if (a != g)
+                assumptions[i] = g;
+            // ignore dep.
+        }        
     }
 }
 
diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h
index 7f8c7dc8f09..4bc09e646a4 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.h
+++ b/src/ast/simplifiers/model_reconstruction_trail.h
@@ -74,13 +74,17 @@ class model_reconstruction_trail {
     scoped_ptr_vector<entry> m_trail;
     unsigned                 m_trail_index = 0;
 
-    void add_vars(dependent_expr const& d, ast_mark& free_vars) {
-        for (expr* t : subterms::all(expr_ref(d.fml(), d.get_manager())))
+    void add_vars(expr* e, ast_mark& free_vars) {
+        for (expr* t : subterms::all(expr_ref(e, m)))
             free_vars.mark(t, true);
     }
+    
+    void add_vars(dependent_expr const& d, ast_mark& free_vars) {
+        add_vars(d.fml(), free_vars);
+    }
 
     bool intersects(ast_mark const& free_vars, dependent_expr const& d) {
-        expr_ref term(d.fml(), d.get_manager());
+        expr_ref term(d.fml(), m);
         auto iter = subterms::all(term);
         return any_of(iter, [&](expr* t) { return free_vars.is_marked(t); });
     }
@@ -126,7 +130,7 @@ class model_reconstruction_trail {
     * register a new depedent expression, update the trail 
     * by removing substitutions that are not equivalence preserving.
     */
-    void replay(unsigned qhead, dependent_expr_state& fmls);
+    void replay(unsigned qhead, expr_ref_vector& assumptions, dependent_expr_state& fmls);
     
     /**
     * retrieve the current model converter corresponding to chaining substitutions from the trail.
diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp
index fd970a44ac5..8060afcd7ac 100644
--- a/src/sat/sat_solver/sat_smt_solver.cpp
+++ b/src/sat/sat_solver/sat_smt_solver.cpp
@@ -70,7 +70,7 @@ class sat_smt_solver : public solver {
             return out;
         }
         void append(generic_model_converter& mc) { model_trail().append(mc); }
-        void replay(unsigned qhead) { m_reconstruction_trail.replay(qhead, *this); }
+        void replay(unsigned qhead, expr_ref_vector& assumptions) { m_reconstruction_trail.replay(qhead, assumptions, *this); }
         void flatten_suffix() override {
             expr_mark seen;
             unsigned j = qhead();
@@ -237,8 +237,10 @@ class sat_smt_solver : public solver {
         expr_ref_vector assumptions(m);
         for (unsigned i = 0; i < sz; ++i)
             assumptions.push_back(ensure_literal(_assumptions[i]));
+        for (expr* a : assumptions)
+            m_preprocess_state.freeze(a); 
         TRACE("sat", tout << assumptions << "\n";);
-        lbool r = internalize_formulas();
+        lbool r = internalize_formulas(assumptions);
         if (r != l_true)
             return r;
 
@@ -271,7 +273,8 @@ class sat_smt_solver : public solver {
 
     void push() override {
         try {
-            internalize_formulas();
+            expr_ref_vector none(m);
+            internalize_formulas(none);
         }
         catch (...) {
             push_internal();
@@ -430,7 +433,7 @@ class sat_smt_solver : public solver {
     }
 
     expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) override {
-        lbool r = internalize_formulas();
+        lbool r = internalize_formulas(vs);
         if (r != l_true) {
             IF_VERBOSE(0, verbose_stream() << "internalize produced " << r << "\n");
             return expr_ref_vector(m);
@@ -561,7 +564,8 @@ class sat_smt_solver : public solver {
 
     void convert_internalized() {
         m_solver.pop_to_base_level();
-        internalize_formulas();        
+        expr_ref_vector none(m);
+        internalize_formulas(none);        
         if (!is_internalized() || m_internalized_converted) 
             return;
         sat2goal s2g;
@@ -641,9 +645,9 @@ class sat_smt_solver : public solver {
             add_assumption(a);
     }
 
-    lbool internalize_formulas() {
+    lbool internalize_formulas(expr_ref_vector& assumptions) {
 
-        if (is_internalized())
+        if (is_internalized() && assumptions.empty())
             return l_true;
 
         unsigned qhead = m_preprocess_state.qhead();
@@ -651,7 +655,7 @@ class sat_smt_solver : public solver {
 
         m_internalized_converted = false;
 
-        m_preprocess_state.replay(qhead);         
+        m_preprocess_state.replay(qhead, assumptions);         
         m_preprocess.reduce();
         if (!m.inc())
             return l_undef;
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index c9b0430b584..8efb433ffaf 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -63,6 +63,11 @@ namespace euf {
         };
         m_egraph.set_display_justification(disp);
 
+        std::function<void(euf::enode* n, euf::enode* ante)> on_literal = [&](enode* n, enode* ante) {
+            propagate_literal(n, ante);
+        };
+        m_egraph.set_on_propagate(on_literal);
+        
         if (m_relevancy.enabled()) {
             std::function<void(euf::enode* root, euf::enode* other)> on_merge =
                 [&](enode* root, enode* other) {
@@ -414,7 +419,6 @@ namespace euf {
             }
             bool propagated1 = false;
             if (m_egraph.propagate()) {
-                propagate_literals();
                 propagate_th_eqs();
                 propagated1 = true;
             }
@@ -435,52 +439,52 @@ namespace euf {
         return propagated;
     }
 
-    void solver::propagate_literals() {
-        for (; m_egraph.has_literal() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_literal()) {
-            auto [n, ante] = m_egraph.get_literal();
-            expr* e = n->get_expr();
-            expr* a = nullptr, *b = nullptr;
-            bool_var v = n->bool_var();
-            SASSERT(m.is_bool(e));
-            size_t cnstr;
-            literal lit;
-            if (!ante) {
-                VERIFY(m.is_eq(e, a, b));
-                cnstr = eq_constraint().to_index();
-                lit = literal(v, false);
-            }
-            else {
-                //
-                // There are the following three cases for propagation of literals
-                // 
-                // 1. n == ante is true from equallity, ante = true/false
-                // 2. n == ante is true from equality, value(ante) != l_undef
-                // 3. value(n) != l_undef, ante = true/false, merge_tf is set on n
-                //
-                lbool val = ante->value();
-                if (val == l_undef) {
-                    SASSERT(m.is_value(ante->get_expr()));
-                    val = m.is_true(ante->get_expr()) ? l_true : l_false;
-                }
-                auto& c = lit_constraint(ante);
-                cnstr = c.to_index();
-                lit = literal(v, val == l_false);
-            }
-            unsigned lvl = s().scope_lvl();
-
-            CTRACE("euf", s().value(lit) != l_true, tout << lit << " " << s().value(lit) << "@" << lvl << " " << mk_bounded_pp(a, m) << " = " << mk_bounded_pp(b, m) << "\n";);
-            if (s().value(lit) == l_false && m_ackerman && a && b) 
-                m_ackerman->cg_conflict_eh(a, b);
-            switch (s().value(lit)) {
-            case l_true:
-                if (n->merge_tf() && !m.is_value(n->get_root()->get_expr())) 
-                    m_egraph.merge(n, ante, to_ptr(lit));
-                break;
-            case l_undef:
-            case l_false:
-                s().assign(lit, sat::justification::mk_ext_justification(lvl, cnstr));
-                break;
+    
+    void solver::propagate_literal(enode* n, enode* ante) {
+        expr* e = n->get_expr();
+        expr* a = nullptr, *b = nullptr;
+        bool_var v = n->bool_var();
+        if (v == sat::null_bool_var)
+            return;
+        SASSERT(m.is_bool(e));
+        size_t cnstr;
+        literal lit;
+        if (!ante) {
+            VERIFY(m.is_eq(e, a, b));
+            cnstr = eq_constraint().to_index();
+            lit = literal(v, false);
+        }
+        else {
+            //
+            // There are the following three cases for propagation of literals
+            // 
+            // 1. n == ante is true from equallity, ante = true/false
+            // 2. n == ante is true from equality, value(ante) != l_undef
+            // 3. value(n) != l_undef, ante = true/false, merge_tf is set on n
+            //
+            lbool val = ante->value();
+            if (val == l_undef) {
+                SASSERT(m.is_value(ante->get_expr()));
+                val = m.is_true(ante->get_expr()) ? l_true : l_false;
             }
+            auto& c = lit_constraint(ante);
+            cnstr = c.to_index();
+            lit = literal(v, val == l_false);
+        }
+        unsigned lvl = s().scope_lvl();
+        
+        CTRACE("euf", s().value(lit) != l_true, tout << lit << " " << s().value(lit) << "@" << lvl << " " << mk_bounded_pp(a, m) << " = " << mk_bounded_pp(b, m) << "\n";);
+        if (s().value(lit) == l_false && m_ackerman && a && b) 
+            m_ackerman->cg_conflict_eh(a, b);
+        switch (s().value(lit)) {
+        case l_true:
+            if (n->merge_tf() && !m.is_value(n->get_root()->get_expr())) 
+                m_egraph.merge(n, ante, to_ptr(lit));
+            break;
+        case l_undef:
+        case l_false:
+            s().assign(lit, sat::justification::mk_ext_justification(lvl, cnstr));
+            break;
         }
     }
 
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 675ec150099..96079fbec92 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -206,7 +206,7 @@ namespace euf {
         void validate_model(model& mdl);
 
         // solving
-        void propagate_literals();
+        void propagate_literal(enode* n, enode* ante);
         void propagate_th_eqs();
         bool is_self_propagated(th_eq const& e);
         void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 01e0aba7c81..d84535a9c86 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -866,6 +866,7 @@ namespace smt {
                 SASSERT(curr != m_false_enode);
                 bool_var v = enode2bool_var(curr);
                 literal l(v, sign);
+                CTRACE("propagate", (get_assignment(l) != l_true), tout << enode_pp(curr, *this) << " " << l << "\n");
                 if (get_assignment(l) != l_true)
                     assign(l, mk_justification(eq_root_propagation_justification(curr)));
                 curr = curr->m_next;
diff --git a/src/tactic/arith/arith_bounds_tactic.h b/src/tactic/arith/arith_bounds_tactic.h
index 4606f61441d..014a6dde34c 100644
--- a/src/tactic/arith/arith_bounds_tactic.h
+++ b/src/tactic/arith/arith_bounds_tactic.h
@@ -27,6 +27,8 @@ Module Name:
     for assembling bounds, but it does not have a way to check for
     subsumption of atoms. 
 
+## Tactic arith-bounds
+
 --*/
 #pragma once
 #include "tactic/tactic.h"
diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp
index eda079e4691..63455864d98 100644
--- a/src/tactic/core/cofactor_elim_term_ite.cpp
+++ b/src/tactic/core/cofactor_elim_term_ite.cpp
@@ -128,9 +128,8 @@ struct cofactor_elim_term_ite::imp {
                     fr.m_first   = false;
                     bool visited = true;
                     if (is_app(t)) {
-                        unsigned num_args = to_app(t)->get_num_args();
-                        for (unsigned i = 0; i < num_args; i++)
-                            visit(to_app(t)->get_arg(i), form_ctx, visited);
+                        for (expr* arg : *to_app(t)) 
+                            visit(arg, form_ctx, visited);
                     }
                     // ignoring quantifiers
                     if (!visited)
@@ -138,16 +137,13 @@ struct cofactor_elim_term_ite::imp {
                 }
                 
                 if (is_app(t)) {
-                    unsigned num_args = to_app(t)->get_num_args();
-                    unsigned i;
-                    for (i = 0; i < num_args; i++) {
-                        if (m_has_term_ite.is_marked(to_app(t)->get_arg(i)))
+                    for (expr* arg : *to_app(t)) {
+                        if (m_has_term_ite.is_marked(arg)) {
+                            m_has_term_ite.mark(t);
+                            TRACE("cofactor", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
+                            save_candidate(t, form_ctx);
                             break;
-                    }
-                    if (i < num_args) {
-                        m_has_term_ite.mark(t);
-                        TRACE("cofactor", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
-                        save_candidate(t, form_ctx);
+                        }
                     }
                 }
                 else {
@@ -284,16 +280,14 @@ struct cofactor_elim_term_ite::imp {
         }
         expr * best = nullptr;
         unsigned best_occs = 0;
-        obj_map<expr, unsigned>::iterator it  = occs.begin();
-        obj_map<expr, unsigned>::iterator end = occs.end();
-        for (; it != end; ++it) {
+        for (auto const& [k, v] : occs) {
             if ((!best) ||
-                (get_depth(it->m_key) < get_depth(best))  ||
-                (get_depth(it->m_key) == get_depth(best) && it->m_value > best_occs) ||
+                (get_depth(k) < get_depth(best))  ||
+                (get_depth(k) == get_depth(best) && v > best_occs) ||
                 // break ties by giving preference to equalities
-                (get_depth(it->m_key) == get_depth(best) && it->m_value == best_occs && m.is_eq(it->m_key) && !m.is_eq(best))) {
-                best = it->m_key;
-                best_occs = it->m_value;
+                (get_depth(k) == get_depth(best) && v == best_occs && m.is_eq(k) && !m.is_eq(best))) {
+                best = k;
+                best_occs = v;                
             }
         }
         visited.reset();
diff --git a/src/tactic/core/cofactor_term_ite_tactic.h b/src/tactic/core/cofactor_term_ite_tactic.h
index e10a310f2ae..68568c8cef1 100644
--- a/src/tactic/core/cofactor_term_ite_tactic.h
+++ b/src/tactic/core/cofactor_term_ite_tactic.h
@@ -8,13 +8,22 @@ Module Name:
 Abstract:
 
     Wrap cofactor_elim_term_ite as a tactic.
-    Eliminate (ground) term if-then-else's using cofactors.
 
 Author:
 
     Leonardo de Moura (leonardo) 2012-02-20.
 
-Revision History:
+Tactic Documentation:
+
+## Tactic cofactor-term-ite
+
+### Short Description
+Eliminate (ground) term if-then-else's using cofactors.
+It hoists nested if-then-else expressions inside terms into the top level of the formula.
+
+### Notes
+
+* does not support proofs, does not support cores
 
 --*/
 #pragma once
diff --git a/src/tactic/core/euf_completion_tactic.h b/src/tactic/core/euf_completion_tactic.h
index 36511bbe343..a1c9166ea23 100644
--- a/src/tactic/core/euf_completion_tactic.h
+++ b/src/tactic/core/euf_completion_tactic.h
@@ -13,6 +13,22 @@ Module Name:
 
     Nikolaj Bjorner (nbjorner) 2022-10-30
 
+Tactic Documentation:
+
+## Tactic euf-completion
+
+### Short Description
+
+Uses the ground equalities as a rewrite system. The formulas are simplified
+using the rewrite system. 
+
+### Long Description
+
+The tactic uses congruence closure to represent and orient the rewrite system. Equalities from the formula
+are inserted in the an E-graph (congruence closure structure) and then a representative that is most shallow
+is extracted.
+
+
 --*/
 #pragma once
 
diff --git a/src/tactic/core/reduce_args_tactic.h b/src/tactic/core/reduce_args_tactic.h
index 615b4d70fc8..749aadd9c06 100644
--- a/src/tactic/core/reduce_args_tactic.h
+++ b/src/tactic/core/reduce_args_tactic.h
@@ -34,31 +34,10 @@ Thus, we replace the $f(t_1, t_2)$ with
 Since $f_a$, $f_b$, $f_c$ are new symbols, satisfiability is preserved.
    
 This transformation is very similar in spirit to the Ackermman's reduction. 
+For each function `f` and argument position of `f` it checks if all occurrences of `f` uses a value at position `i`.
+The values may be different, but all occurrences have to be values for the reduction to be applicable. 
+It creates a fresh function for each of the different values at position `i`.
 
-This transformation should work in the following way:
-
-```
-   1- Create a mapping decl2arg_map from declarations to tuples of booleans, an entry [f -> (true, false, true)]
-       means that f is a declaration with 3 arguments where the first and third arguments are always values.
-   2- Traverse the formula and populate the mapping. 
-        For each function application f(t1, ..., tn) do
-          a) Create a boolean tuple (is_value(t1), ..., is_value(tn)) and do
-             the logical-and with the tuple that is already in the mapping. If there is no such tuple
-             in the mapping, we just add a new entry.
-
-   If all entries are false-tuples, then there is nothing to be done. The transformation is not applicable.
-
-   Now, we create a mapping decl2new_decl from (decl, val_1, ..., val_n) to decls. Note that, n may be different for each entry,
-   but it is the same for the same declaration.
-   For example, suppose we have [f -> (true, false, true)] in decl2arg_map, 
-  and applications f(1, a, 2), f(1, b, 2), f(1, b, 3), f(2, b, 3), f(2, c, 3) in the formula.
-   Then, decl2arg_map would contain
-        (f, 1, 2) -> f_1_2
-        (f, 1, 3) -> f_1_3
-        (f, 2, 3) -> f_2_3
-   where f_1_2, f_1_3 and f_2_3 are new function symbols.
-   Using the new map, we can replace the occurrences of f.
-```
 
 ### Example
  
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index 667d53626b9..bd2f58b442e 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -865,11 +865,11 @@ class tseitin_cnf_tactic : public tactic {
 
     void collect_param_descrs(param_descrs & r) override {
         insert_max_memory(r);
-        r.insert("common_patterns", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns");
-        r.insert("distributivity", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas");
-        r.insert("distributivity_blowup", CPK_UINT, "(default: 32) maximum overhead for applying distributivity during CNF encoding");
-        r.insert("ite_chaing", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains");                                                       
-        r.insert("ite_extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas");
+        r.insert("common_patterns", CPK_BOOL, "minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns", "true");
+        r.insert("distributivity", CPK_BOOL, "minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas", "true");
+        r.insert("distributivity_blowup", CPK_UINT, "maximum overhead for applying distributivity during CNF encoding", "32");
+        r.insert("ite_chaing", CPK_BOOL, "minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains", "true");                                                       
+        r.insert("ite_extra", CPK_BOOL, "add redundant clauses (that improve unit propagation) when encoding if-then-else formulas", "true");
     }
     
     void operator()(goal_ref const & in, goal_ref_buffer & result) override {
diff --git a/src/tactic/fpa/fpa2bv_tactic.h b/src/tactic/fpa/fpa2bv_tactic.h
index 0845aafa200..57b6d498529 100644
--- a/src/tactic/fpa/fpa2bv_tactic.h
+++ b/src/tactic/fpa/fpa2bv_tactic.h
@@ -5,15 +5,16 @@ Module Name:
 
     fpa2bv_tactic.h
 
-Abstract:
-
-    Tactic that converts floating points to bit-vectors
-
 Author:
 
     Christoph (cwinter) 2012-02-09
 
-Notes:
+Tactic Documentation:
+
+## Tactic fpa2bv
+
+### Short Description
+Converts floating points to bit-vector representation.
 
 --*/
 #pragma once
diff --git a/src/tactic/fpa/qffp_tactic.h b/src/tactic/fpa/qffp_tactic.h
index e4c8eb38699..fb1a46afd5f 100644
--- a/src/tactic/fpa/qffp_tactic.h
+++ b/src/tactic/fpa/qffp_tactic.h
@@ -13,8 +13,17 @@ Module Name:
 
     Christoph (cwinter) 2012-01-16
 
-Notes:
+Tactic Documentation:
 
+## Tactic qffp
+
+### Short Description 
+Tactic for QF_FP formulas
+
+## Tactic qffpbv
+
+### Short Description 
+Tactic for QF_FPBV formulas
 
 --*/
 #pragma once
diff --git a/src/tactic/fpa/qffplra_tactic.h b/src/tactic/fpa/qffplra_tactic.h
index af862db2997..543e6f23afe 100644
--- a/src/tactic/fpa/qffplra_tactic.h
+++ b/src/tactic/fpa/qffplra_tactic.h
@@ -14,7 +14,8 @@ Module Name:
 
     Christoph (cwinter) 2018-04-24
 
-Notes:
+
+## Tactic qffplra
 
 
 --*/