diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 642983737..cdc771f12 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -433,12 +433,14 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
     }
 #ifdef DATATYPE_V2
     if (get_dtutil().is_datatype(s)) {
-        ptr_buffer<format> fs;
         unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s);
-        for (unsigned i = 0; i < sz; i++) {
-            fs.push_back(pp_sort(get_dtutil().get_datatype_parameter_sort(s, i)));
+        if (sz > 0) {
+            ptr_buffer<format> fs;            
+            for (unsigned i = 0; i < sz; i++) {
+                fs.push_back(pp_sort(get_dtutil().get_datatype_parameter_sort(s, i)));
+            }
+            return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str());        
         }
-        return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str());        
     }
 #endif
     return format_ns::mk_string(get_manager(), s->get_name().str().c_str());
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 7ad80336d..1090b3ff1 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -858,22 +858,18 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
     ptr_vector<func_decl> const & constructors = *get_datatype_constructors(ty);
     // step 1)
     unsigned sz = constructors.size();
-    ++m_start;
+    unsigned start = ++m_start;
     for (unsigned j = 0; j < sz; ++j) {        
-        func_decl * c = constructors[(j + m_start) % sz];
+        func_decl * c = constructors[(j + start) % sz];
         unsigned num_args = c->get_arity();
         unsigned i = 0;
-        for (; i < num_args; i++) {
-            sort * T_i = c->get_domain(i);
-            if (is_datatype(T_i))
-                break;
-        }
+        for (; i < num_args && !is_datatype(c->get_domain(i)); i++) {};
         if (i == num_args)
             return c;
     }
     // step 2)
     for (unsigned j = 0; j < sz; ++j) {        
-        func_decl * c = constructors[(j + m_start) % sz];
+        func_decl * c = (*constructors)[(j + start) % sz];
         TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";);
         unsigned num_args = c->get_arity();
         unsigned i = 0;
diff --git a/src/ast/datatype_decl_plugin2.cpp b/src/ast/datatype_decl_plugin2.cpp
index fa3c73bca..bd7b41a88 100644
--- a/src/ast/datatype_decl_plugin2.cpp
+++ b/src/ast/datatype_decl_plugin2.cpp
@@ -847,6 +847,7 @@ namespace datatype {
         r = 0;
         ptr_vector<sort> forbidden_set;
         forbidden_set.push_back(ty);
+        TRACE("util_bug", tout << "invoke get-non-rec: " << sort_ref(ty, m) << "\n";);
         r = get_non_rec_constructor_core(ty, forbidden_set);
         SASSERT(forbidden_set.back() == ty);
         SASSERT(r);
@@ -866,46 +867,53 @@ namespace datatype {
         //   1) T_i's are not recursive
         // If there is no such constructor, then we select one that 
         //   2) each type T_i is not recursive or contains a constructor that does not depend on T
+
         ptr_vector<func_decl> const& constructors = *get_datatype_constructors(ty);
-        // step 1)
         unsigned sz = constructors.size();
-        ++m_start;
+        TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n";
+              tout << "forbidden: ";
+              for (sort* s : forbidden_set) tout << sort_ref(s, m) << " ";
+              tout << "\n";
+              tout << "constructors: " << sz << "\n";
+              for (func_decl* f : constructors) tout << func_decl_ref(f, m) << "\n";
+              );
+        // step 1)
+        unsigned start = ++m_start;
         for (unsigned j = 0; j < sz; ++j) {        
-            func_decl * c = constructors[(j + m_start) % sz];
+            func_decl * c = constructors[(j + start) % sz];
+            TRACE("util_bug", tout << "checking " << sort_ref(ty, m) << ": " << func_decl_ref(c, m) << "\n";);
             unsigned num_args = c->get_arity();
             unsigned i = 0;
-            for (; i < num_args; i++) {
-                sort * T_i = c->get_domain(i);
-                if (is_datatype(T_i))
-                    break;
-            }
-            if (i == num_args)
+            for (; i < num_args && !is_datatype(c->get_domain(i)); i++);
+            if (i == num_args) {
+                TRACE("util_bug", tout << "found non-rec " << func_decl_ref(c, m) << "\n";);
                 return c;
+            }
         }
         // step 2)
         for (unsigned j = 0; j < sz; ++j) {        
-            func_decl * c = constructors[(j + m_start) % sz];
-            TRACE("util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";);
+            func_decl * c = constructors[(j + start) % sz];
+            TRACE("util_bug", tout << "non_rec_constructor c: " << j << " " << func_decl_ref(c, m) << "\n";);
             unsigned num_args = c->get_arity();
             unsigned i = 0;
             for (; i < num_args; i++) {
                 sort * T_i = c->get_domain(i);
-                TRACE("util_bug", tout << "c: " << c->get_name() << " i: " << i << " T_i: " << T_i->get_name() << "\n";);
+                TRACE("util_bug", tout << "c: " << i << " " << sort_ref(T_i, m) << "\n";);
                 if (!is_datatype(T_i)) {
-                    TRACE("util_bug", tout << "T_i is not a datatype\n";);
+                    TRACE("util_bug", tout << sort_ref(T_i, m) << " is not a datatype\n";);
                     continue;
                 }
                 if (std::find(forbidden_set.begin(), forbidden_set.end(), T_i) != forbidden_set.end()) {
-                    TRACE("util_bug", tout << "T_i is in forbidden_set\n";);
+                    TRACE("util_bug", tout << sort_ref(T_i, m) << " is in forbidden_set\n";);
                     break;
                 }
                 forbidden_set.push_back(T_i);
                 func_decl * nested_c = get_non_rec_constructor_core(T_i, forbidden_set);
                 SASSERT(forbidden_set.back() == T_i);
                 forbidden_set.pop_back();
-                TRACE("util_bug", tout << "nested_c: " << nested_c->get_name() << "\n";);
                 if (nested_c == 0)
                     break;
+                TRACE("util_bug", tout << "nested_c: " << nested_c->get_name() << "\n";);
             }
             if (i == num_args)
                 return c;
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 997d5671e..13cb52df1 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1952,7 +1952,7 @@ bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr*
         }
     }
 
-    if (szr == 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) {
+    if (szr == 1 && szl >= 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) {
         return solve_itos(szr, rs, szl, ls, rhs, lhs, is_sat);
     }
 
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 0b6ad2c82..1f9dd91d1 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -248,6 +248,7 @@ struct goal2sat::imp {
                 for (unsigned i = 0; i < num; ++i) {
                     m_result_stack[i].neg();
                 }                
+                mk_clause(m_result_stack.size(), m_result_stack.c_ptr());
             }
             else {
                 for (unsigned i = 0; i < num; ++i) {
@@ -278,6 +279,7 @@ struct goal2sat::imp {
             if (sign)
                 l.neg();
             m_result_stack.push_back(l);
+            TRACE("goal2sat", tout << m_result_stack << "\n";);
         }
     }
 
diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h
index ea00cb71c..d0db105d3 100644
--- a/src/smt/asserted_formulas.h
+++ b/src/smt/asserted_formulas.h
@@ -220,6 +220,8 @@ class asserted_formulas {
     unsigned depth(expr* e) { return m_expr2depth[e]; }
     bool pull_cheap_ite_trees();
 
+    void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
+
 public:
     asserted_formulas(ast_manager & m, smt_params & p);
     ~asserted_formulas();
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 79a1f0416..cb1465d94 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -348,10 +348,8 @@ namespace smt {
         literal_vector & antecedents = m_tmp_literal_vector;
         antecedents.reset();
         justification2literals_core(js, antecedents);
-        literal_vector::iterator it  = antecedents.begin();
-        literal_vector::iterator end = antecedents.end();
-        for(; it != end; ++it)
-            process_antecedent(*it, num_marks);
+        for (literal l : antecedents)
+            process_antecedent(l, num_marks);
     }
 
     /**
@@ -517,11 +515,13 @@ namespace smt {
             }
 
             TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
-                  tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";);
+                  tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n";
+                  );
             SASSERT(js != null_b_justification);
             switch (js.get_kind()) {
             case b_justification::CLAUSE: {
                 clause * cls = js.get_clause();
+                TRACE("conflict", m_ctx.display_clause_detail(tout, cls););
                 if (cls->is_lemma())
                     cls->inc_clause_activity();
                 unsigned num_lits = cls->get_num_literals();
@@ -566,7 +566,7 @@ namespace smt {
                 if (m_ctx.is_marked(l.var()))
                     break;
                 CTRACE("conflict", m_ctx.get_assign_level(l) != m_conflict_lvl && m_ctx.get_assign_level(l) != m_ctx.get_base_level(),
-                       tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal(tout, l);
+                       tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal_verbose(tout, l);
                        tout << "\n";);
                 SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl ||
                         // it may also be an (out-of-order) asserted literal