diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 7df849b81..608d42005 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1467,10 +1467,7 @@ namespace nlsat {
             m_result = &result;
             svector<literal> lits;
             TRACE("nlsat", tout << "project x" << x << "\n"; 
-                  for (unsigned i = 0; i < num; ++i) {
-                      m_solver.display(tout, ls[i]) << " ";
-                  }
-                  tout << "\n";
+                  m_solver.display(tout, num, ls);
                   m_solver.display(tout););
                   
             DEBUG_CODE(
@@ -1514,12 +1511,7 @@ namespace nlsat {
                 result.set(i, ~result[i]);
             }
             DEBUG_CODE(
-                TRACE("nlsat", 
-                      for (literal l : result) {
-                          m_solver.display(tout << " ", l);
-                      }
-                      tout << "\n";
-                      );
+                TRACE("nlsat", m_solver.display(tout, result.size(), result.c_ptr()); );
                 for (literal l : result) {
                     CTRACE("nlsat", l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
                     SASSERT(l_true == m_solver.value(l));
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index f1a89db0b..c5a5eec8e 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -3282,6 +3282,12 @@ namespace nlsat {
         m_imp->m_bvalues.reset();
         m_imp->m_bvalues.append(vs);
         m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef);        
+        for (unsigned i = 0; i < m_imp->m_atoms.size(); ++i) {
+            atom* a = m_imp->m_atoms[i];
+            if (a) {
+                m_imp->m_bvalues[i] = to_lbool(m_imp->m_evaluator.eval(a, false));
+            }
+        }
         TRACE("nlsat", display(tout););
     }
     
@@ -3329,6 +3335,10 @@ namespace nlsat {
         return out;
     }
 
+    std::ostream& solver::display(std::ostream & out, literal_vector const& ls) const {
+        return display(out, ls.size(), ls.c_ptr());
+    }
+
     std::ostream& solver::display(std::ostream & out, var x) const {
         return m_imp->m_display_var(out, x);
     }
diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h
index fa9d45b05..25ce35e6f 100644
--- a/src/nlsat/nlsat_solver.h
+++ b/src/nlsat/nlsat_solver.h
@@ -241,6 +241,8 @@ namespace nlsat {
 
         std::ostream& display(std::ostream & out, unsigned n, literal const* ls) const;
 
+        std::ostream& display(std::ostream & out, literal_vector const& ls) const;
+
         std::ostream& display(std::ostream & out, atom const& a) const;
 
         /**
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index f585507f6..81e1c9ce8 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -25,6 +25,7 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "ast/for_each_expr.h"
 #include "ast/rewriter/rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/rewriter/quant_hoist.h"
 #include "qe/nlqsat.h"
@@ -617,7 +618,7 @@ namespace qe {
 
          */
 
-        void ackermanize_div(expr_ref& fml) {
+        void ackermanize_div(expr_ref& fml, expr_ref_vector& paxioms) {
             is_pure_proc is_pure(*this);
             {
                 expr_fast_mark1 visited;
@@ -626,10 +627,8 @@ namespace qe {
             if (is_pure.has_divs()) {
                 arith_util arith(m);
                 proof_ref pr(m);
-                expr_ref_vector paxioms(m);
                 div_rewriter_star rw(*this);
                 rw(fml, fml, pr);
-                paxioms.push_back(fml);
                 vector<div> const& divs = rw.divs();
                 for (unsigned i = 0; i < divs.size(); ++i) {
                     expr_ref den_is0(m.mk_eq(divs[i].den, arith.mk_real(0)), m);
@@ -640,7 +639,6 @@ namespace qe {
                                                   m.mk_eq(divs[i].name, divs[j].name)));
                     }
                 }
-                fml = mk_and(paxioms);
             }
         }
 
@@ -669,14 +667,16 @@ namespace qe {
         // expr -> nlsat::solver
 
         void hoist(expr_ref& fml) {
-            ackermanize_div(fml);
+            expr_ref_vector paxioms(m);
+            ackermanize_div(fml, paxioms);
             quantifier_hoister hoist(m);
             vector<app_ref_vector> qvars;
             app_ref_vector vars(m);
             bool is_forall = false;   
             pred_abs abs(m);
 
-            abs.get_free_vars(fml, vars);
+            expr_ref fml_a(m.mk_and(fml, mk_and(paxioms)), m);
+            abs.get_free_vars(fml_a, vars);
             insert_set(m_free_vars, vars);
             qvars.push_back(vars); 
             vars.reset();  
@@ -706,6 +706,9 @@ namespace qe {
             fml = m.mk_iff(is_true, fml);
             goal_ref g = alloc(goal, m);
             g->assert_expr(fml);
+            for (expr* f : paxioms) {
+                g->assert_expr(f);
+            }
             expr_dependency_ref core(m);
             goal_ref_buffer result;
             (*m_nftactic)(g, result);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 970a4e485..d6d81fc11 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2338,6 +2338,13 @@ bool theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
           display_deps(tout, dep); 
           );
 
+    TRACE("seq", 
+          tout << "assert: " 
+          << mk_bounded_pp(n1->get_owner(), m) << " = " << mk_bounded_pp(n2->get_owner(), m) << " <-\n"
+          << lits << "\n";
+          );
+
+
     justification* js = ctx.mk_justification(
         ext_theory_eq_propagation_justification(
             get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
@@ -2473,7 +2480,24 @@ bool theory_seq::solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs
     return false;
 }
 
-bool theory_seq::solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
+bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
+    rational n; 
+    expr* s = nullptr, *idx = nullptr;
+    if (ls.size() == 1 && m_util.str.is_nth_i(ls[0], s, idx)) {
+        expr_ref lhs(m_util.str.mk_at(s, idx), m);
+        expr_ref rhs(m_util.str.mk_concat(rs.size(), rs.c_ptr()), m);
+        expr_ref_vector ls1(m); ls1.push_back(lhs);
+        expr_ref_vector rs1(m); rs1.push_back(m_util.str.mk_unit(rhs));
+        m_eqs.push_back(eq(m_eq_id++, ls1, rs1, deps));        
+        return true;
+    }   
+    return false;
+}
+
+bool theory_seq::solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
+    if (solve_nth_eq2(ls, rs, dep)) {
+        return true;
+    }
     if (ls.size() != 1 || rs.size() <= 1) {
         return false;
     }
@@ -2649,10 +2673,10 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
         TRACE("seq", tout << "binary\n";);
         return true;
     }
-    if (!ctx.inconsistent() && solve_nth_eq(ls, rs, deps)) {
+    if (!ctx.inconsistent() && solve_nth_eq1(ls, rs, deps)) {
         return true;
     }
-    if (!ctx.inconsistent() && solve_nth_eq(rs, ls, deps)) {
+    if (!ctx.inconsistent() && solve_nth_eq1(rs, ls, deps)) {
         return true;
     }
     if (!ctx.inconsistent() && solve_itos(rs, ls, deps)) {
@@ -5557,6 +5581,11 @@ bool theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
     TRACE("seq_verbose",
           tout << "assert: " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << " <- \n";
           if (!lits.empty()) { ctx.display_literals_verbose(tout, lits) << "\n"; });
+
+    TRACE("seq",
+          tout << "assert: " << mk_bounded_pp(e1, m) << " = " << mk_bounded_pp(e2, m) << " <- \n";
+          tout << lits << "\n";);
+
     justification* js =
         ctx.mk_justification(
             ext_theory_eq_propagation_justification(
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 9d0854aa0..6be5b3b2c 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -488,7 +488,8 @@ namespace smt {
         bool lift_ite(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
         bool solve_unit_eq(expr* l, expr* r, dependency* dep);
         bool solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
-        bool solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
+        bool solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
+        bool solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
         bool solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
         bool is_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, expr_ref& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr_ref& y);
         bool is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index e8e996396..bf4df2770 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -49,6 +49,7 @@ Author:
 Notes:
 
 --*/
+#include "ast/ast_pp.h"
 #include "tactic/tactical.h"
 #include "tactic/goal_shared_occs.h"
 #include "tactic/generic_model_converter.h"
@@ -268,6 +269,7 @@ class tseitin_cnf_tactic : public tactic {
                 !m.is_or(c1, c1, c2))
                 return false;
             
+            SASSERT(to_app(n)->get_num_args() == 3);
             swap_if_gt(a1, a2);
             swap_if_gt(b1, b2);
             swap_if_gt(c1, c2);
@@ -834,6 +836,8 @@ class tseitin_cnf_tactic : public tactic {
             m_produce_models      = g->models_enabled();
             m_produce_unsat_cores = g->unsat_core_enabled(); 
 
+            TRACE("tseitin_cnf", g->display(tout););
+
             m_occs(*g);
             reset_cache();
             m_deps.reset();