diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index b969a53d9..00a08df00 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1575,19 +1575,6 @@ bool ast_manager::are_equal(expr * a, expr * b) const {
     return false;
 }
 
-void ast_manager::inc_ref(ast * n) {
-    if (n) {
-        n->inc_ref();
-    }
-}
-
-void ast_manager::dec_ref(ast* n) {
-    if (n) {
-        n->dec_ref();
-        if (n->get_ref_count() == 0)
-            delete_node(n);
-    }
-}
 
 bool ast_manager::are_distinct(expr* a, expr* b) const {
     if (is_app(a) && is_app(b)) {
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 3f941b8d1..47ea0f812 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1571,9 +1571,19 @@ public:
 
     void debug_ref_count() { m_debug_ref_count = true; }
 
-    void inc_ref(ast * n);
-
-    void dec_ref(ast * n); 
+    void inc_ref(ast * n) {
+        if (n) {
+            n->inc_ref();
+        }
+    }
+    
+    void dec_ref(ast* n) {
+        if (n) {
+            n->dec_ref();
+            if (n->get_ref_count() == 0)
+                delete_node(n);
+        }
+    }
 
     template<typename T>
     void inc_array_ref(unsigned sz, T * const * a) {
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 450bfbf5b..f5e92fe57 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -28,6 +28,7 @@ Notes:
 #include"eval_cmd.h"
 #include"gparams.h"
 #include"env_params.h"
+#include"well_sorted.h"
 
 class help_cmd : public cmd {
     svector<symbol> m_cmds;
@@ -156,11 +157,16 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
     pr = ctx.get_check_sat_result()->get_proof();
     if (pr == 0)
         throw cmd_exception("proof is not available");
+    if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) {
+        throw cmd_exception("proof is not well sorted");
+    }
+    
     // TODO: reimplement a new SMT2 pretty printer 
     ast_smt_pp pp(ctx.m());
     cmd_is_declared isd(ctx);
     pp.set_is_declared(&isd);
     pp.set_logic(ctx.get_logic());
+    // ctx.regular_stream() << mk_pp(pr, ctx.m()) << "\n";
     pp.display_smt2(ctx.regular_stream(), pr);
     ctx.regular_stream() << std::endl;
 });
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 7cd67b10a..89f08d3df 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -242,6 +242,7 @@ void theory_seq::init(context* ctx) {
 }
 
 final_check_status theory_seq::final_check_eh() {
+    m_new_propagation = false;
     TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
     if (simplify_and_solve_eqs()) {
         ++m_stats.m_solve_eqs;
@@ -1436,7 +1437,7 @@ bool theory_seq::solve_eqs(unsigned i) {
             change = true;
         }
     }
-    return change || ctx.inconsistent();
+    return change || m_new_propagation || ctx.inconsistent();
 }
 
 bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) {
@@ -1831,8 +1832,6 @@ bool theory_seq::solve_ne(unsigned idx) {
             continue;
         }
         else {
-
-
             if (!updated) {
                 for (unsigned j = 0; j < i; ++j) {
                     new_ls.push_back(n.ls(j));
@@ -2120,7 +2119,6 @@ bool theory_seq::explain_empty(expr_ref_vector& es, dependency*& dep) {
 
 bool theory_seq::simplify_and_solve_eqs() {
     context & ctx = get_context();
-    m_new_propagation = false;
     m_new_solution = true;
     while (m_new_solution && !ctx.inconsistent()) {
         m_new_solution = false;
@@ -2639,6 +2637,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
     else if (m_util.str.is_itos(e, e1)) {
         rational val;
         if (get_value(e1, val)) {
+            TRACE("seq", tout << mk_pp(e, m) << " -> " << val << "\n";);
             expr_ref num(m), res(m);
             num = m_autil.mk_numeral(val, true);
             if (!ctx.e_internalized(num)) {
@@ -2652,6 +2651,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
                 deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(n1, n2)));
             }
             else {
+                TRACE("seq", tout << "add axiom\n";);                
                 add_axiom(~mk_eq(num, e1, false), mk_eq(e, res, false));
                 add_axiom(mk_eq(num, e1, false), ~mk_eq(e, res, false));
                 result = e;