Merge branch 'master' of https://github.com/Z3Prover/z3 into lackr

src/ast/expr2polynomial.cpp

@@ -23,6 +23,7 @@ Notes:
 #include"ast_smt2_pp.h"
 #include"z3_exception.h"
 #include"cooperate.h"
+#include"common_msgs.h"
 
 struct expr2polynomial::imp {
     struct frame {
@@ -94,7 +95,7 @@ struct expr2polynomial::imp {
 
     void checkpoint() {
         if (m_cancel)
-            throw default_exception("canceled");
+            throw default_exception(Z3_CANCELED_MSG);
         cooperate("expr2polynomial");
     }
 

src/ast/rewriter/seq_rewriter.cpp

@@ -1484,6 +1484,7 @@ bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr
         if (is_sat) {
             lhs.push_back(concat_non_empty(szl, l));
             rhs.push_back(concat_non_empty(szr, r));
+            //split_units(lhs, rhs);
         }
         return true;
     }
@@ -1492,13 +1493,39 @@ bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr
         if (is_sat) {
             lhs.push_back(concat_non_empty(szl, l));
             rhs.push_back(concat_non_empty(szr, r));
+            //split_units(lhs, rhs);
         }
         return true;
     }    
-    
     return false;
 }
 
+void seq_rewriter::split_units(expr_ref_vector& lhs, expr_ref_vector& rhs) {
+    expr* a, *b, *a1, *b1, *a2, *b2;
+    while (true) {
+        if (m_util.str.is_unit(lhs.back(), a) &&
+            m_util.str.is_unit(rhs.back(), b)) {
+            lhs[lhs.size()-1] = a;
+            rhs[rhs.size()-1] = b;
+            break;
+        }
+        if (m_util.str.is_concat(lhs.back(), a, a2) && 
+            m_util.str.is_unit(a, a1) && 
+            m_util.str.is_concat(rhs.back(), b, b2) &&
+            m_util.str.is_unit(b, b1)) {
+            expr_ref _pin_a(lhs.back(), m()), _pin_b(rhs.back(), m());
+            lhs[lhs.size()-1] = a1;
+            rhs[rhs.size()-1] = b1;
+            lhs.push_back(a2);
+            rhs.push_back(b2);
+        }
+        else {
+            break;
+        }
+    }
+}
+
+
 bool seq_rewriter::is_epsilon(expr* e) const {
     expr* e1;
     return m_util.re.is_to_re(e, e1) && m_util.str.is_empty(e1);

src/ast/rewriter/seq_rewriter.h

@@ -113,6 +113,7 @@ class seq_rewriter {
     bool is_sequence(expr* e, expr_ref_vector& seq);
     bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
     bool is_epsilon(expr* e) const;
+    void split_units(expr_ref_vector& lhs, expr_ref_vector& rhs);
 
 public:    
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):

src/math/interval/interval_def.h

@@ -24,6 +24,7 @@ Revision History:
 #include"trace.h"
 #include"scoped_numeral.h"
 #include"cooperate.h"
+#include"common_msgs.h"
 
 #define DEFAULT_PI_PRECISION 2
 
@@ -63,7 +64,7 @@ void interval_manager<C>::del(interval & a) {
 template<typename C>
 void interval_manager<C>::checkpoint() {
     if (!m_limit.inc())
-        throw default_exception("canceled");
+        throw default_exception(Z3_CANCELED_MSG);
     cooperate("interval");
 }
 

src/math/polynomial/algebraic_numbers.cpp

@@ -26,6 +26,7 @@ Notes:
 #include"mpbqi.h"
 #include"timeit.h"
 #include"algebraic_params.hpp"
+#include"common_msgs.h"
 
 namespace algebraic_numbers {
 
@@ -126,7 +127,7 @@ namespace algebraic_numbers {
 
         void checkpoint() {
             if (!m_limit.inc())
-                throw algebraic_exception("canceled");
+                throw algebraic_exception(Z3_CANCELED_MSG);
             cooperate("algebraic");
         }
 

src/math/polynomial/polynomial.cpp

@@ -34,6 +34,7 @@ Notes:
 #include"linear_eq_solver.h"
 #include"scoped_numeral_buffer.h"
 #include"ref_buffer.h"
+#include"common_msgs.h"
 
 namespace polynomial {
 
@@ -2374,7 +2375,7 @@ namespace polynomial {
 
         void checkpoint() {
             if (!m_limit.inc()) {
-                throw polynomial_exception("canceled");
+                throw polynomial_exception(Z3_CANCELED_MSG);
             }
             cooperate("polynomial");
         }

src/math/polynomial/upolynomial.cpp

@@ -26,6 +26,7 @@ Notes:
 #include"polynomial_primes.h"
 #include"buffer.h"
 #include"cooperate.h"
+#include"common_msgs.h"
 
 namespace upolynomial {
 
@@ -155,7 +156,7 @@ namespace upolynomial {
 
     void core_manager::checkpoint() {
         if (!m_limit.inc())
-            throw upolynomial_exception("canceled");
+            throw upolynomial_exception(Z3_CANCELED_MSG);
         cooperate("upolynomial");
     }
 

src/math/realclosure/realclosure.cpp

@@ -29,6 +29,7 @@ Notes:
 #include"ref_vector.h"
 #include"ref_buffer.h"
 #include"cooperate.h"
+#include"common_msgs.h"
 
 #ifndef REALCLOSURE_INI_BUFFER_SIZE
 #define REALCLOSURE_INI_BUFFER_SIZE 32
@@ -548,7 +549,7 @@ namespace realclosure {
 
         void checkpoint() {
             if (!m_limit.inc())
-                throw exception("canceled");
+                throw exception(Z3_CANCELED_MSG);
             cooperate("rcf");
         }
 

src/math/subpaving/subpaving_t_def.h

@@ -460,7 +460,7 @@ context_t<C>::~context_t() {
 template<typename C>
 void context_t<C>::checkpoint() {
     if (!m_limit.inc())
-        throw default_exception("canceled");
+        throw default_exception(Z3_CANCELED_MSG);
     if (memory::get_allocation_size() > m_max_memory)
         throw default_exception(Z3_MAX_MEMORY_MSG);
     cooperate("subpaving");

src/math/subpaving/tactic/expr2subpaving.cpp

@@ -24,6 +24,7 @@ Notes:
 #include"cooperate.h"
 #include"arith_decl_plugin.h"
 #include"scoped_numeral_buffer.h"
+#include"common_msgs.h"
 
 struct expr2subpaving::imp {
     struct frame {
@@ -94,7 +95,7 @@ struct expr2subpaving::imp {
 
     void checkpoint() {
         if (m().canceled())
-            throw default_exception("canceled");
+            throw default_exception(Z3_CANCELED_MSG);
         cooperate("expr2subpaving");
     }
 

src/muz/bmc/dl_bmc_engine.cpp

@@ -1510,7 +1510,7 @@ namespace datalog {
 
     void bmc::checkpoint() {
         if (m.canceled()) {
-            throw default_exception("bmc canceled");
+            throw default_exception(Z3_CANCELED_MSG);
         }
     }
 

src/muz/duality/duality_dl_interface.cpp

@@ -328,7 +328,7 @@ namespace Duality {
             ans = rs->Solve();
         }
         catch (Duality::solver::cancel_exception &exn){
-            throw default_exception("duality canceled");
+            throw default_exception(Z3_CANCELED_MSG);
         }
         catch (Duality::Solver::Incompleteness &exn){
             throw default_exception("incompleteness");

src/muz/pdr/pdr_context.cpp

@@ -1911,7 +1911,7 @@ namespace pdr {
 
     void context::checkpoint() {
         if (m.canceled()) {
-            throw default_exception("pdr canceled");
+            throw default_exception(Z3_CANCELED_MSG);
         }
     }
 

src/smt/arith_eq_adapter.cpp

@@ -81,14 +81,6 @@ namespace smt {
         }
     };
 
-    arith_simplifier_plugin * arith_eq_adapter::get_simplifier() {
-        if (!m_as) {
-            simplifier & s = get_context().get_simplifier();
-            m_as = static_cast<arith_simplifier_plugin*>(s.get_plugin(m_owner.get_family_id()));
-        }
-        return m_as;
-    }
-
     void arith_eq_adapter::mk_axioms(enode * n1, enode * n2) {
         SASSERT(n1 != n2);
         ast_manager & m = get_manager();
@@ -103,6 +95,9 @@ namespace smt {
             // We don't need to create axioms for 2 = 3
             return; 
         }
+        if (t1 == t2) {
+            return;
+        }
         
         context & ctx = get_context();
         CTRACE("arith_eq_adapter_relevancy", !(ctx.is_relevant(n1) && ctx.is_relevant(n2)),
@@ -192,6 +187,7 @@ namespace smt {
         // Old version that used to be buggy.
         // I fixed the theory arithmetic internalizer to accept non simplified terms of the form t1 - t2 
         // if t1 and t2 already have slacks (theory variables) associated with them.
+        // It also accepts terms with repeated variables (Issue #429).
         app * le = 0;
         app * ge = 0;
         if (m_util.is_numeral(t1))
@@ -202,9 +198,10 @@ namespace smt {
         }        
         else {
             sort * st       = m.get_sort(t1);
-            app * minus_one = m_util.mk_numeral(rational::minus_one(), st);
+            app_ref minus_one(m_util.mk_numeral(rational::minus_one(), st), m);
-            app * zero      = m_util.mk_numeral(rational::zero(), st);
+            app_ref zero(m_util.mk_numeral(rational::zero(), st), m);
-            app_ref s(m_util.mk_add(t1, m_util.mk_mul(minus_one, t2)), m);
+            app_ref t3(m_util.mk_mul(minus_one, t2), m);
+            app_ref s(m_util.mk_add(t1, t3), m);
             le              = m_util.mk_le(s, zero);
             ge              = m_util.mk_ge(s, zero);
         }

src/smt/arith_eq_adapter.h

@@ -75,8 +75,6 @@ namespace smt {
         ast_manager & get_manager() const { return m_owner.get_manager(); }
         enode * get_enode(theory_var v) const { return m_owner.get_enode(v); }
 
-        arith_simplifier_plugin * get_simplifier();
-
     public:
         arith_eq_adapter(theory & owner, theory_arith_params & params, arith_util & u):m_owner(owner), m_params(params), m_util(u), m_as(0) {}
         void new_eq_eh(theory_var v1, theory_var v2);

src/smt/tactic/smt_tactic.cpp

@@ -225,7 +225,7 @@ public:
                 }
             }
             if (m_ctx->canceled()) {
-                throw tactic_exception("smt_tactic canceled");
+                throw tactic_exception(Z3_CANCELED_MSG);
             }
 
             lbool r;

src/smt/theory_arith.h

@@ -450,6 +450,9 @@ namespace smt {
         svector<theory_var>     m_nl_propagated;    // non linear monomials that became linear
         v_dependency_manager    m_dep_manager;      // for tracking bounds during non-linear reasoning
 
+        vector<uint_set>        m_row_vars;         // variables in a given row. Used during internalization to detect repeated variables.
+        unsigned                m_row_vars_top;
+
         var_heap                m_to_patch;         // heap containing all variables v s.t. m_value[v] does not satisfy bounds of v.
         nat_set                 m_left_basis;       // temporary: set of variables that already left the basis in make_feasible
         bool                    m_blands_rule;
@@ -583,6 +586,9 @@ namespace smt {
         void mk_enode_if_reflect(app * n);
         template<bool invert>
         void add_row_entry(unsigned r_id, numeral const & coeff, theory_var v);
+        uint_set& row_vars();
+        class scoped_row_vars;
+        
         void internalize_internal_monomial(app * m, unsigned r_id);
         theory_var internalize_add(app * n);
         theory_var internalize_mul_core(app * m);

src/smt/theory_arith_core.h

@@ -197,6 +197,15 @@ namespace smt {
         }
     }
 
+    /**
+       \brief access the current set of variables associated with row.
+     */
+    template<typename Ext>
+    uint_set& theory_arith<Ext>::row_vars() {
+        SASSERT(m_row_vars_top > 0);
+        return m_row_vars[m_row_vars_top-1];
+    }
+
     /**
        \brief Add coeff * v to the row r.
        The column is also updated.
@@ -206,6 +215,26 @@ namespace smt {
     void theory_arith<Ext>::add_row_entry(unsigned r_id, numeral const & coeff, theory_var v) {
         row    & r          = m_rows[r_id];
         column & c          = m_columns[v];
+        if (row_vars().contains(v)) {
+            typename vector<row_entry>::iterator it = r.begin_entries();
+            typename vector<row_entry>::iterator end = r.end_entries();
+            bool found = false;
+            for (; !found && it != end; ++it) {
+                SASSERT(!it->is_dead());
+                if (it->m_var == v) {
+                    if (invert) {
+                        it->m_coeff -= coeff;
+                    }
+                    else {
+                        it->m_coeff += coeff;
+                    }
+                    found = true;
+                }
+            }
+            SASSERT(found);
+            return;
+        }
+        row_vars().insert(v);
         int r_idx;
         row_entry & r_entry = r.add_row_entry(r_idx);
         int c_idx;
@@ -238,12 +267,13 @@ namespace smt {
             }
         }
         rational _val; 
-        if (m_util.is_mul(m) && m_util.is_numeral(m->get_arg(0), _val)) {
+        expr* arg1, *arg2;
+        if (m_util.is_mul(m, arg1, arg2) && m_util.is_numeral(arg1, _val)) {
             SASSERT(m->get_num_args() == 2);
             numeral val(_val);
-            theory_var v = internalize_term_core(to_app(m->get_arg(1)));
+            theory_var v = internalize_term_core(to_app(arg2));
             if (reflection_enabled()) {
-                internalize_term_core(to_app(m->get_arg(0)));
+                internalize_term_core(to_app(arg1));
                 mk_enode(m);
             }
             add_row_entry<true>(r_id, val, v);
@@ -264,6 +294,7 @@ namespace smt {
         CTRACE("internalize_add_bug", n->get_num_args() == 2 && n->get_arg(0) == n->get_arg(1), tout << "n: " << mk_pp(n, get_manager()) << "\n";);
         SASSERT(m_util.is_add(n));
         unsigned r_id = mk_row();
+        scoped_row_vars _sc(m_row_vars, m_row_vars_top);
         unsigned num_args = n->get_num_args();
         for (unsigned i = 0; i < num_args; i++) {
             internalize_internal_monomial(to_app(n->get_arg(i)), r_id);
@@ -324,6 +355,7 @@ namespace smt {
             numeral val(_val);
             SASSERT(!val.is_one());
             unsigned r_id = mk_row();
+            scoped_row_vars _sc(m_row_vars, m_row_vars_top);
             if (reflection_enabled())
                 internalize_term_core(to_app(m->get_arg(0)));
             theory_var v = internalize_mul_core(to_app(m->get_arg(1)));
@@ -617,6 +649,7 @@ namespace smt {
         enode * e      = mk_enode(n);
         theory_var r   = mk_var(e);
         unsigned r_id = mk_row();
+        scoped_row_vars _sc(m_row_vars, m_row_vars_top);
         add_row_entry<true>(r_id, numeral(1), arg);
         add_row_entry<false>(r_id, numeral(1), r);
         init_row(r_id);
@@ -644,6 +677,25 @@ namespace smt {
         return v;
     }
 
+    template<typename Ext>
+    class theory_arith<Ext>::scoped_row_vars {
+        unsigned& m_top;
+    public:
+        scoped_row_vars(vector<uint_set>& row_vars, unsigned& top):
+            m_top(top)
+        {
+            SASSERT(row_vars.size() >= top);
+            if (row_vars.size() == top) {
+                row_vars.push_back(uint_set());
+            }
+            row_vars[top].reset();
+            ++m_top;
+        }
+        ~scoped_row_vars() {
+            --m_top;            
+        }
+    };
+
     /**
        \brief Internalize the given term and return an alias for it.
        Return null_theory_var if the term was not implemented by the theory yet.
@@ -1579,6 +1631,7 @@ namespace smt {
         m_liberal_final_check(true),
         m_changed_assignment(false),
         m_assume_eq_head(0),
+        m_row_vars_top(0),
         m_nl_rounds(0),
         m_nl_gb_exhausted(false),
         m_nl_new_exprs(m),

src/smt/theory_seq.cpp

@@ -533,11 +533,14 @@ bool theory_seq::is_eq(expr* e, expr*& a, expr*& b) const {
         (a = to_app(e)->get_arg(0), b = to_app(e)->get_arg(1), true);
 }
 
-
 bool theory_seq::is_pre(expr* e, expr*& s, expr*& i) {
     return is_skolem(m_pre, e) && (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1), true);
 }
 
+bool theory_seq::is_post(expr* e, expr*& s, expr*& i) {
+    return is_skolem(m_post, e) && (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1), true);
+}
+
 
 
 expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
@@ -782,6 +785,9 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
     if (lhs.empty()) {
         return true;
     }
+    TRACE("seq", 
+          tout << ls << " = " << rs << "\n";
+          tout << lhs << " = " << rhs << "\n";);
     for (unsigned i = 0; !ctx.inconsistent() && i < lhs.size(); ++i) {
         expr_ref li(lhs[i].get(), m);
         expr_ref ri(rhs[i].get(), m);
@@ -789,7 +795,6 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
             // no-op
         }
         else if (m_util.is_seq(li) || m_util.is_re(li)) {
-            reduce_length(li, ri);
             m_eqs.push_back(mk_eqdep(li, ri, deps));            
         }
         else {
@@ -817,16 +822,11 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const&
     return false;
 }
 
-bool theory_seq::reduce_length(expr* l, expr* r) {
+bool theory_seq::reduce_length(expr* l, expr* r, literal_vector& lits) {
-    expr* l2, *r2;
     expr_ref len1(m), len2(m);
-    literal_vector lits;
+    lits.reset();
-    m_util.str.is_concat(l, l, l2);
-    m_util.str.is_concat(r, r, r2);
     if (get_length(l, len1, lits) &&
         get_length(r, len2, lits) && len1 == len2) {
-        TRACE("seq", tout << "Propagate equal lengths\n";);
-        //propagate_eq(lits, l, r, true);
         return true;
     }
     else {
@@ -914,8 +914,8 @@ bool theory_seq::solve_eqs(unsigned i) {
                 eq e1 = m_eqs[m_eqs.size()-1];
                 m_eqs.set(i, e1);
                 --i;
-                ++m_stats.m_num_reductions;
             }
+            ++m_stats.m_num_reductions;
             m_eqs.pop_back();
             change = true;
         }
@@ -945,6 +945,10 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
         TRACE("seq", tout << "unit\n";);
         return true;
     }
+    if (!ctx.inconsistent() && reduce_length_eq(ls, rs, deps)) {
+        TRACE("seq", tout << "length\n";);
+        return true;
+    }
     if (!ctx.inconsistent() && solve_binary_eq(ls, rs, deps)) {
         TRACE("seq", tout << "binary\n";);
         return true;
@@ -990,6 +994,43 @@ bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const&
     return false;
 }
 
+bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
+    if (ls.empty() || rs.empty()) {
+        return false;
+    }
+    if (ls.size() <= 1 && rs.size() <= 1) {
+        return false;
+    }
+    SASSERT(ls.size() > 1 || rs.size() > 1);
+
+    literal_vector lits;
+    expr_ref l(ls[0], m), r(rs[0], m);
+    if (reduce_length(l, r, lits)) {
+        expr_ref_vector lhs(m), rhs(m);
+        lhs.append(ls.size()-1, ls.c_ptr() + 1);
+        rhs.append(rs.size()-1, rs.c_ptr() + 1);
+        SASSERT(!lhs.empty() || !rhs.empty());
+        m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
+        TRACE("seq", tout << "Propagate equal lengths " << l << " " << r << "\n";);
+        propagate_eq(deps, lits, l, r, true);
+        return true;
+    }
+
+    l = ls.back(); r = rs.back();
+    if (reduce_length(l, r, lits)) {
+        expr_ref_vector lhs(m), rhs(m);
+        lhs.append(ls.size()-1, ls.c_ptr());
+        rhs.append(rs.size()-1, rs.c_ptr());
+        SASSERT(!lhs.empty() || !rhs.empty());
+        m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
+        TRACE("seq", tout << "Propagate equal lengths " << l << " " << r << "\n";);
+        propagate_eq(deps, lits, l, r, true);
+        return true;
+    }
+
+    return false;
+ }
+
 bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
     context& ctx = get_context();
     ptr_vector<expr> xs, ys;
@@ -1064,51 +1105,78 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
 bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
     context& ctx = get_context();
     expr* s, *i, *l;
+    rational r;
     if (m_util.str.is_extract(e, s, i, l)) {
         // 0 <= i <= len(s), 0 <= l, i + l <= len(s)
         expr_ref zero(m_autil.mk_int(0), m);        
         expr_ref ls(m_util.str.mk_length(s), m);
         expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m);
-        literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
+        bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
+        literal i_ge_0 = i_is_zero?true_literal:mk_literal(m_autil.mk_ge(i, zero));
         literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
         literal li_ge_ls  = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero));
         literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
+        literal _lits[4] = { i_ge_0, i_lt_len_s, li_ge_ls, l_ge_zero };
         if (ctx.get_assignment(i_ge_0) == l_true &&
             ctx.get_assignment(i_lt_len_s) == l_true && 
             ctx.get_assignment(li_ge_ls) == l_true &&
             ctx.get_assignment(l_ge_zero) == l_true) {
             len = l;
-            lits.push_back(i_ge_0); lits.push_back(i_lt_len_s); lits.push_back(li_ge_ls); lits.push_back(l_ge_zero);
+            lits.append(4, _lits);
             return true;
         }
+        TRACE("seq", tout << mk_pp(e, m) << "\n"; ctx.display_literals_verbose(tout, 4, _lits); tout << "\n";
+              for (unsigned i = 0; i < 4; ++i) tout << ctx.get_assignment(_lits[i]) << "\n";);
     }
     else if (m_util.str.is_at(e, s, i)) {
         // has length 1 if 0 <= i < len(s)
         expr_ref zero(m_autil.mk_int(0), m);
-        literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
+        bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
+        literal i_ge_0 = i_is_zero?true_literal:mk_literal(m_autil.mk_ge(i, zero));
         literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
+        literal _lits[2] = { i_ge_0, i_lt_len_s};
         if (ctx.get_assignment(i_ge_0) == l_true &&
             ctx.get_assignment(i_lt_len_s) == l_true) {
             len = m_autil.mk_int(1);
-            lits.push_back(i_ge_0); lits.push_back(i_lt_len_s);
+            lits.append(2, _lits);
             return true;
         }
+        TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
     }
     else if (is_pre(e, s, i)) {
         expr_ref zero(m_autil.mk_int(0), m);
-        literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
+        bool i_is_zero = m_autil.is_numeral(i, r) && r.is_zero();
+        literal i_ge_0 = i_is_zero?true_literal:mk_literal(m_autil.mk_ge(i, zero));
         literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
+        literal _lits[2] = { i_ge_0, i_lt_len_s };
         if (ctx.get_assignment(i_ge_0) == l_true &&
             ctx.get_assignment(i_lt_len_s) == l_true) {
             len = i;
-            lits.push_back(i_ge_0); lits.push_back(i_lt_len_s);
+            lits.append(2, _lits);
             return true;
         }
+        TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
+    }
+    else if (is_post(e, s, l)) {
+        expr_ref zero(m_autil.mk_int(0), m);
+        literal l_ge_0 = mk_literal(m_autil.mk_ge(l, zero));
+        literal l_le_len_s = mk_literal(m_autil.mk_ge(mk_sub(m_util.str.mk_length(s), l), zero));
+        literal _lits[2] = { l_ge_0, l_le_len_s };
+        if (ctx.get_assignment(l_ge_0) == l_true && 
+            ctx.get_assignment(l_le_len_s) == l_true) {
+            len = l;
+            lits.append(2, _lits);
+            return true;
+        }
+        TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
     }
     else if (m_util.str.is_unit(e)) {
         len = m_autil.mk_int(1);
         return true;
     }
+    else {
+        TRACE("seq", tout << "unhandled: " << mk_pp(e, m) << "\n";);
+    }
     return false;    
 }
 
@@ -2526,10 +2594,10 @@ bool theory_seq::is_skolem(symbol const& s, expr* e) const {
 void theory_seq::propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs) {
     literal_vector lits;
     lits.push_back(lit);
-    propagate_eq(lits, e1, e2, add_to_eqs);
+    propagate_eq(0, lits, e1, e2, add_to_eqs);
 }
 
-void theory_seq::propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs) {
+void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, expr* e1, expr* e2, bool add_to_eqs) {
     context& ctx = get_context();
 
     enode* n1 = ensure_enode(e1);
@@ -2539,10 +2607,14 @@ void theory_seq::propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bo
     }
     ctx.mark_as_relevant(n1);
     ctx.mark_as_relevant(n2);
+    
+    literal_vector lits(_lits);
+    enode_pair_vector eqs;
+    linearize(deps, eqs, lits);
+
     if (add_to_eqs) {
-        dependency* deps = 0;
+        for (unsigned i = 0; i < _lits.size(); ++i) {
-        for (unsigned i = 0; i < lits.size(); ++i) {
+            literal lit = _lits[i];
-            literal lit = lits[i];
             SASSERT(l_true == ctx.get_assignment(lit));
             deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit)));
         }
@@ -2554,7 +2626,7 @@ void theory_seq::propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bo
     justification* js =
         ctx.mk_justification(
             ext_theory_eq_propagation_justification(
-                get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), 0, 0, n1, n2));
+                get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
 
     m_new_propagation = true;
     ctx.assign_eq(n1, n2, eq_justification(js));

src/smt/theory_seq.h

@@ -335,7 +335,8 @@ namespace smt {
         bool propagate_max_length(expr* l, expr* r, dependency* dep);
 
         bool get_length(expr* s, expr_ref& len, literal_vector& lits);
-        bool reduce_length(expr* l, expr* r);
+        bool reduce_length(expr* l, expr* r, literal_vector& lits);
+        bool reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps);
 
         expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); }
         expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); }
@@ -365,7 +366,7 @@ namespace smt {
         void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
         void propagate_eq(dependency* dep, enode* n1, enode* n2);
         void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs);
-        void propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs);
+        void propagate_eq(dependency* dep, literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs);
         void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
 
         u_map<unsigned> m_branch_start;
@@ -384,6 +385,7 @@ namespace smt {
         bool is_tail(expr* a, expr*& s, unsigned& idx) const;
         bool is_eq(expr* e, expr*& a, expr*& b) const; 
         bool is_pre(expr* e, expr*& s, expr*& i);
+        bool is_post(expr* e, expr*& s, expr*& i);
         expr_ref mk_nth(expr* s, expr* idx);
         expr_ref mk_last(expr* e);
         expr_ref mk_first(expr* e);

src/tactic/nlsat_smt/nl_purify_tactic.cpp

@@ -289,7 +289,7 @@ private:
 
     void check_point() {
         if (m.canceled()) {
-            throw tactic_exception("canceled");
+            throw tactic_exception(Z3_CANCELED_MSG);
         }
     }