fixes for #2513

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/seq_rewriter.cpp

@@ -21,6 +21,7 @@ Notes:
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "ast/ast_util.h"
 #include "util/uint_set.h"
 #include "math/automata/automaton.h"
@@ -546,7 +547,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case _OP_STRING_STRIDOF: 
         UNREACHABLE();
     }
-    CTRACE("seq", st != BR_FAILED, tout << result << "\n";);
+    CTRACE("seq_verbose", st != BR_FAILED, tout << result << "\n";);
     return st;
 }
 
@@ -643,14 +644,38 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
         result = m_autil.mk_add(es.size(), es.c_ptr());
         return BR_REWRITE2;
     }
+    expr* c = nullptr, *t = nullptr, *e = nullptr;
+    if (m().is_ite(a, c, t, e) && (t->get_ref_count() == 1 || e->get_ref_count() == 1)) {
+        result = m().mk_ite(c, m_util.str.mk_length(t), m_util.str.mk_length(e));
+        return BR_REWRITE3;
+    }
+#if 0
+    expr* s = nullptr, *offs = nullptr, *l = nullptr;
+    // len(extract(s, offs, len(s) - offs)) = max(0, len(s) - offs)
+    // 
+    if (m_util.str.is_extract(a, s, offs, l) && is_suffix(s, offs, l)) {
+        expr_ref zero(m_autil.mk_int(0), m());
+        result = m_autil.mk_sub(m_util.str.mk_length(s), offs);
+        result = m().mk_ite(m_autil.mk_ge(result, zero), result, zero);
+        return BR_REWRITE_FULL;
+    }
+#endif
     return BR_FAILED;
 }
 
+bool seq_rewriter::is_suffix(expr* s, expr* offset, expr* len) {
+    expr_ref_vector lens(m());
+    rational a, b;
+    return 
+        get_lengths(len, lens, a) && 
+        (a.neg(), m_autil.is_numeral(offset, b) && b.is_pos() && a == b);
+}
+
 br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result) {
     zstring s;
     rational pos, len;
 
-    TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << " " << mk_pp(c, m()) << "\n";);
+    TRACE("seq_verbose", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << " " << mk_pp(c, m()) << "\n";);
     bool constantBase = m_util.str.is_string(a, s);
     bool constantPos = m_autil.is_numeral(b, pos);
     bool constantLen = m_autil.is_numeral(c, len);
@@ -702,7 +727,8 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         m_lhs.reset();
         expr_ref_vector lens(m());
         m_util.str.get_concat(a, m_lhs);
-        if (!get_lengths(b, lens, pos)) {
+        TRACE("seq", tout << m_lhs << " " << pos << " " << lens << "\n";);
+        if (!get_lengths(b, lens, pos) || pos.is_neg()) {
             return BR_FAILED;
         }
         unsigned i = 0;
@@ -742,10 +768,21 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
 
     // (extract s 0 (len s)) = s 
     expr* a2 = nullptr;
-    if (_pos == 0 && m_util.str.is_length(c, a2) && a == a2) {
+    if (_pos == 0 && m_util.str.is_length(c, a2)) {
-        result = a;
+        m_lhs.reset();
+        m_util.str.get_concat(a, m_lhs);
+        if (!m_lhs.empty() && m_lhs.get(0) == a2) {
+            result = a2;
             return BR_DONE;
         }
+    }
+
+    expr* a1 = nullptr, *b1 = nullptr, *c1 = nullptr;
+    if (m_util.str.is_extract(a, a1, b1, c1) && 
+        is_suffix(a1, b1, c1) && is_suffix(a, b, c)) {
+        result = m_util.str.mk_substr(a1, m_autil.mk_add(b1, b), m_autil.mk_sub(c1, b));
+        return BR_REWRITE3;
+    }
 
     unsigned offset = 0;
     for (; offset < as.size() && m_util.str.is_unit(as.get(offset)) && offset < _pos; ++offset) {};
@@ -799,7 +836,7 @@ bool seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, rational& pos) {
     else {
         return false;
     }
-    return !pos.is_neg();
+    return true;
 }
 
 bool seq_rewriter::cannot_contain_suffix(expr* a, expr* b) {
@@ -992,9 +1029,28 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
 }
 
 br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
+
+    rational pos1, pos2;
+    expr* s = nullptr, *p = nullptr, *len = nullptr;
+    if (m_util.str.is_unit(a, s) && m_autil.is_numeral(b, pos1) && pos1.is_zero()) {
+        result = s;
+        return BR_DONE;
+    }
+    if (m_util.str.is_extract(a, s, p, len) && m_autil.is_numeral(p, pos1)) {
+        expr_ref_vector lens(m());
+        rational pos2;
+        if (get_lengths(len, lens, pos2) && (pos1 == -pos2) && (lens.size() == 1) && (lens.get(0) == s)) {
+            expr_ref idx(m_autil.mk_int(pos1), m());
+            idx = m_autil.mk_add(b, idx);
+            expr* es[2] = { s, idx };
+            result = m().mk_app(m_util.get_family_id(), OP_SEQ_NTH, 2, es);
+            return BR_REWRITE_FULL;
+        }
+    }
+
     expr* es[2] = { a, b};
     expr* la = m_util.str.mk_length(a);
-    result = m().mk_ite(m().mk_and(m_autil.mk_le(m_autil.mk_int(0), b), m_autil.mk_lt(b, la)), 
+    result = m().mk_ite(m().mk_and(m_autil.mk_ge(b, m_autil.mk_int(0)), m().mk_not(m_autil.mk_ge(b, la))), 
                         m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_I, 2, es), 
                         m().mk_app(m_util.get_family_id(), OP_SEQ_NTH_U, 2, es));
     return BR_REWRITE_FULL;
@@ -1078,10 +1134,26 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
         result = a;
         return BR_DONE;
     }
+    if (a == b) {
+        result = c;
+        return BR_DONE;
+    }
     if (m_util.str.is_empty(b)) {
         result = m_util.str.mk_concat(c, a);
         return BR_REWRITE1;
     }
+    
+    if (m_util.str.is_string(b, s2)) {
+        m_lhs.reset();
+        m_util.str.get_concat(a, m_lhs);
+        if (!m_lhs.empty() && m_util.str.is_string(m_lhs.get(0), s1) && 
+            s1.contains(s2)) {
+            m_lhs[0] = m_util.str.mk_string(s1.replace(s2, s3));
+            result = m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr());
+            return BR_REWRITE1;
+        }
+    }
+
     return BR_FAILED;
 }
 
@@ -1835,7 +1907,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
     zstring s;
     bool lchange = false;
     SASSERT(lhs.empty());
-    TRACE("seq", tout << ls << "\n"; tout << rs << "\n";);
+    TRACE("seq_verbose", tout << ls << "\n"; tout << rs << "\n";);
     // solve from back
     while (true) {
         while (!rs.empty() && m_util.str.is_empty(rs.back())) {
@@ -1943,7 +2015,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
         else {
             break;
         }
-        TRACE("seq", tout << ls << " == " << rs << "\n";);
+        TRACE("seq_verbose", tout << ls << " == " << rs << "\n";);
        
         change = true;
         lchange = true;
@@ -2106,7 +2178,7 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
         return true;
     }
     else {
-        TRACE("seq", tout << mk_pp(l, m()) << " != " << mk_pp(r, m()) << "\n";);
+        TRACE("seq", tout << mk_bounded_pp(l, m()) << " != " << mk_bounded_pp(r, m()) << "\n";);
         return false;
     }
 }

src/ast/rewriter/seq_rewriter.h

@@ -139,6 +139,8 @@ class seq_rewriter {
     bool cannot_contain_prefix(expr* a, expr* b);
     bool cannot_contain_suffix(expr* a, expr* b);
 
+    bool is_suffix(expr* s, expr* offset, expr* len);
+
     bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs);
     bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, 
                         expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);

src/ast/static_features.cpp

@@ -346,9 +346,7 @@ void static_features::update_core(expr * e) {
                 m_num_uninterpreted_functions++;
         }
         if (!_is_eq && !_is_gate) {
-            unsigned num_args = to_app(e)->get_num_args();
+            for (expr * arg : *to_app(e)) {
-            for (unsigned i = 0; i < num_args; i++) {
-                expr * arg   = to_app(e)->get_arg(i);
                 sort * arg_s = m_manager.get_sort(arg); 
                 if (!m_manager.is_uninterp(arg_s)) {
                     family_id fid_arg = arg_s->get_family_id();

src/cmd_context/cmd_context.cpp

@@ -36,6 +36,7 @@ Notes:
 #include "ast/rewriter/var_subst.h"
 #include "ast/pp.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "ast/decl_collector.h"
 #include "ast/well_sorted.h"
 #include "ast/for_each_expr.h"
@@ -1896,7 +1897,7 @@ void cmd_context::validate_model() {
                     continue;
                 }
                 TRACE("model_validate", model_smt2_pp(tout, *this, *md, 0););
-                IF_VERBOSE(10, verbose_stream() << "model check failed on: " << mk_pp(a, m()) << "\n";);                
+                analyze_failure(evaluator, a, true);
                 IF_VERBOSE(11, model_smt2_pp(verbose_stream(), *this, *md, 0););                
                 invalid_model = true;
             }
@@ -1907,6 +1908,73 @@ void cmd_context::validate_model() {
     }
 }
 
+void cmd_context::analyze_failure(model_evaluator& ev, expr* a, bool expected_value) {
+    if (expected_value && m().is_and(a)) {
+        for (expr* arg : *to_app(a)) {
+            if (ev.is_false(arg)) {
+                analyze_failure(ev, arg, true);
+                return;
+            }
+        }
+    }
+    expr* c = nullptr, *t = nullptr, *e = nullptr;
+    if (expected_value && m().is_ite(a, c, t, e)) {
+        if (ev.is_true(c) && ev.is_false(t)) {
+            analyze_failure(ev, t, true);
+            return;
+        }
+        if (ev.is_false(c) && ev.is_false(e)) {
+            analyze_failure(ev, e, true);
+            return;
+        }
+    }
+    if (m().is_not(a, e)) {
+        analyze_failure(ev, e, !expected_value);
+        return;
+    }
+    if (!expected_value && m().is_or(a)) {
+        for (expr* arg : *to_app(a)) {
+            if (ev.is_false(arg)) {
+                analyze_failure(ev, arg, false);
+                return;
+            }
+        }
+    }
+    if (!expected_value && m().is_ite(a, c, t, e)) {
+        if (ev.is_true(c) && ev.is_true(t)) {
+            analyze_failure(ev, t, false);
+            return;
+        }
+        if (ev.is_false(c) && ev.is_true(e)) {
+            analyze_failure(ev, e, false);
+            return;
+        }
+    }
+    IF_VERBOSE(10, verbose_stream() << "model check failed on: " << " " << mk_pp(a, m()) << "\n";);                
+    IF_VERBOSE(10, verbose_stream() << "expected value: " << (expected_value?"true":"false") << "\n";);                
+
+    IF_VERBOSE(10, display_detailed_analysis(verbose_stream(), ev, a));
+}
+
+void cmd_context::display_detailed_analysis(std::ostream& out, model_evaluator& ev, expr* e) {
+    ptr_vector<expr> es;
+    es.push_back(e);
+    expr_mark visited;
+    for (unsigned i = 0; i < es.size(); ++i) {
+        e = es[i];
+        if (visited.is_marked(e)) {
+            continue;
+        }
+        visited.mark(e, true);
+        expr_ref val = ev(e);
+        out << "#" << e->get_id() << ": " << mk_bounded_pp(e, m(), 1) << " " << val << "\n";
+        if (is_app(e)) {
+            for (expr* arg : *to_app(e)) {
+                es.push_back(arg);
+            }
+        }
+    }
+}
 
 void cmd_context::mk_solver() {
     bool proofs_enabled, models_enabled, unsat_core_enabled;

src/cmd_context/cmd_context.h

@@ -367,6 +367,8 @@ public:
     check_sat_state cs_state() const;
     void complete_model(model_ref& mdl) const;
     void validate_model();
+    void analyze_failure(model_evaluator& ev, expr* e, bool expected_value);
+    void display_detailed_analysis(std::ostream& out, model_evaluator& ev, expr* e);
     void display_model(model_ref& mdl);
 
     void register_plugin(symbol const & name, decl_plugin * p, bool install_names);

src/qe/nlqsat.cpp

@@ -641,6 +641,7 @@ namespace qe {
                     }
                 }
                 fml = mk_and(paxioms);
+                std::cout << fml << "\n";
             }
         }
 

src/sat/sat_config.cpp

@@ -181,6 +181,7 @@ namespace sat {
         m_drat_file       = p.drat_file();
         m_drat            = (m_drat_check_unsat || m_drat_file != symbol("") || m_drat_check_sat) && p.threads() == 1;
         m_drat_binary     = p.drat_binary();
+        m_drat_activity   = p.drat_activity();
         m_dyn_sub_res     = p.dyn_sub_res();
 
         // Parameters used in Liang, Ganesh, Poupart, Czarnecki AAAI 2016.

src/sat/sat_config.h

@@ -168,6 +168,7 @@ namespace sat {
         symbol             m_drat_file;
         bool               m_drat_check_unsat;
         bool               m_drat_check_sat;
+        bool               m_drat_activity;
         
         bool               m_card_solver;
         bool               m_xor_solver;

src/sat/sat_drat.cpp

@@ -31,12 +31,15 @@ namespace sat {
         m_inconsistent(false),
         m_check_unsat(false),
         m_check_sat(false),
-        m_check(false)
+        m_check(false),
+        m_activity(false),
+        m_num_add(0), 
+        m_num_del(0)
     {
-        if (s.m_config.m_drat && s.m_config.m_drat_file != symbol()) {
+        if (s.get_config().m_drat && s.get_config().m_drat_file != symbol()) {
-            auto mode = s.m_config.m_drat_binary ? (std::ios_base::binary | std::ios_base::out | std::ios_base::trunc) : std::ios_base::out;
+            auto mode = s.get_config().m_drat_binary ? (std::ios_base::binary | std::ios_base::out | std::ios_base::trunc) : std::ios_base::out;
-            m_out = alloc(std::ofstream, s.m_config.m_drat_file.str().c_str(), mode);
+            m_out = alloc(std::ofstream, s.get_config().m_drat_file.str().c_str(), mode);
-            if (s.m_config.m_drat_binary) {
+            if (s.get_config().m_drat_binary) {
                 std::swap(m_out, m_bout);
             }
         }
@@ -59,9 +62,10 @@ namespace sat {
     }
 
     void drat::updt_config() {
-        m_check_unsat = s.m_config.m_drat_check_unsat;
+        m_check_unsat = s.get_config().m_drat_check_unsat;
-        m_check_sat = s.m_config.m_drat_check_sat;
+        m_check_sat = s.get_config().m_drat_check_sat;
         m_check = m_check_unsat || m_check_sat;
+        m_activity = s.get_config().m_drat_activity;
     }
 
     std::ostream& operator<<(std::ostream& out, drat::status st) {
@@ -78,6 +82,9 @@ namespace sat {
         if (st == status::asserted || st == status::external) {
             return;
         }
+        if (m_activity && ((m_num_add % 1000) == 0)) {
+            dump_activity();
+        }
         
         char buffer[10000];
         char digits[20];     // enough for storing unsigned
@@ -114,6 +121,14 @@ namespace sat {
 	m_out->write(buffer, len);               
     }
 
+    void drat::dump_activity() {
+        (*m_out) << "c a ";
+        for (unsigned v = 0; v < s.num_vars(); ++v) {
+            (*m_out) << s.m_activity[v] << " ";
+        }
+        (*m_out) << "\n";
+    }
+
     void drat::bdump(unsigned n, literal const* c, status st) {
         unsigned char ch = 0;
         switch (st) {
@@ -648,6 +663,7 @@ namespace sat {
     }
 
     void drat::add() {
+        ++m_num_add;
         if (m_out) (*m_out) << "0\n";
         if (m_bout) bdump(0, nullptr, status::learned);
         if (m_check_unsat) {
@@ -655,12 +671,14 @@ namespace sat {
         }
     }
     void drat::add(literal l, bool learned) {
+        ++m_num_add;
         status st = get_status(learned);
         if (m_out) dump(1, &l, st);
         if (m_bout) bdump(1, &l, st);
         if (m_check) append(l, st);
     }
     void drat::add(literal l1, literal l2, bool learned) {
+        ++m_num_add;
         literal ls[2] = {l1, l2};
         status st = get_status(learned);
         if (m_out) dump(2, ls, st);
@@ -668,6 +686,7 @@ namespace sat {
         if (m_check) append(l1, l2, st);
     }
     void drat::add(clause& c, bool learned) {
+        ++m_num_add;
         status st = get_status(learned);
         if (m_out) dump(c.size(), c.begin(), st);
         if (m_bout) bdump(c.size(), c.begin(), st);
@@ -677,6 +696,7 @@ namespace sat {
         }
     }
     void drat::add(literal_vector const& lits, svector<premise> const& premises) {
+        ++m_num_add;
         if (m_check) {
             switch (lits.size()) {
             case 0: add(); break;
@@ -690,6 +710,7 @@ namespace sat {
         }                        
     }
     void drat::add(literal_vector const& c) {
+        ++m_num_add;
         if (m_out) dump(c.size(), c.begin(), status::learned);
         if (m_bout) bdump(c.size(), c.begin(), status::learned);
         if (m_check) {
@@ -708,12 +729,14 @@ namespace sat {
     }
 
     void drat::del(literal l) {
+        ++m_num_del;
         if (m_out) dump(1, &l, status::deleted);
         if (m_bout) bdump(1, &l, status::deleted);
         if (m_check_unsat) append(l, status::deleted);
     }
 
     void drat::del(literal l1, literal l2) {
+        ++m_num_del;
         literal ls[2] = {l1, l2};
         SASSERT(!(l1 == literal(13923, false) && l2 == literal(14020, true)));
         if (m_out) dump(2, ls, status::deleted);
@@ -733,7 +756,7 @@ namespace sat {
             m_seen[lit.index()] = false;
         }
 #endif
-
+        ++m_num_del;
         //SASSERT(!(c.size() == 2 && c[0] == literal(13923, false) && c[1] == literal(14020, true)));
         if (m_out) dump(c.size(), c.begin(), status::deleted);
         if (m_bout) bdump(c.size(), c.begin(), status::deleted);

src/sat/sat_drat.h

@@ -54,8 +54,10 @@ namespace sat {
         vector<watch>           m_watches;
         svector<lbool>          m_assignment;
         bool                    m_inconsistent;
-        bool                    m_check_unsat, m_check_sat, m_check;
+        unsigned                m_num_add, m_num_del;
+        bool                    m_check_unsat, m_check_sat, m_check, m_activity;
 
+        void dump_activity();
         void dump(unsigned n, literal const* c, status st);
         void bdump(unsigned n, literal const* c, status st);
         void append(literal l, status st);

src/sat/sat_params.pyg

@@ -48,6 +48,7 @@ def_module_params('sat',
                           ('drat.binary', BOOL, False, 'use Binary DRAT output format'),
                           ('drat.check_unsat', BOOL, False, 'build up internal proof and check'),
                           ('drat.check_sat', BOOL, False, 'build up internal trace, check satisfying model'),
+                          ('drat.activity', BOOL, False, 'dump variable activities'),
                           ('cardinality.solver', BOOL, True, 'use cardinality solver'),
                           ('pb.solver', SYMBOL, 'solver', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), binary_merge, segmented, solver (use native solver)'),
                           ('pb.min_arity', UINT, 9, 'minimal arity to compile pb/cardinality constraints to CNF'),

src/sat/sat_solver.cpp

@@ -885,10 +885,9 @@ namespace sat {
             uint64_t age = m_stats.m_conflict - m_canceled[v];
             if (age > 0) {
                 double decay = pow(0.95, age);
-                m_activity[v] = static_cast<unsigned>(m_activity[v] * decay);
+                set_activity(v, static_cast<unsigned>(m_activity[v] * decay));
                 // NB. MapleSAT does not update canceled.
                 m_canceled[v] = m_stats.m_conflict;
-                m_case_split_queue.activity_changed_eh(v, false);
             }
         }
         
@@ -1532,8 +1531,7 @@ namespace sat {
                 next = m_case_split_queue.min_var();
                 auto age = m_stats.m_conflict - m_canceled[next];
                 while (age > 0) {
-                    m_activity[next] = static_cast<unsigned>(m_activity[next] * pow(0.95, age));
+                    set_activity(next, static_cast<unsigned>(m_activity[next] * pow(0.95, age)));
-                    m_case_split_queue.activity_changed_eh(next, false);
                     m_canceled[next] = m_stats.m_conflict;
                     next = m_case_split_queue.min_var();
                     age = m_stats.m_conflict - m_canceled[next];                    
@@ -1792,10 +1790,12 @@ namespace sat {
         return tracking_assumptions() && m_assumption_set.contains(l);
     }
 
-    void solver::set_activity(bool_var v, unsigned act) {
+    void solver::set_activity(bool_var v, unsigned new_act) {
         unsigned old_act = m_activity[v];
-        m_activity[v] = act; 
+        m_activity[v] = new_act; 
-        m_case_split_queue.activity_changed_eh(v, act > old_act);
+        if (!was_eliminated(v) && value(v) == l_undef && new_act != old_act) {
+            m_case_split_queue.activity_changed_eh(v, new_act > old_act);
+        }
     }
 
     bool solver::is_assumption(bool_var v) const {
@@ -2195,14 +2195,9 @@ namespace sat {
         }
     }
 
-
     void solver::update_activity(bool_var v, double p) {
-        unsigned old_act = m_activity[v];
         unsigned new_act = (unsigned) (num_vars() * m_config.m_activity_scale *  p);
-        m_activity[v] = new_act;
+        set_activity(v, new_act);
-        if (!was_eliminated(v) && value(v) == l_undef && new_act != old_act) {
-            m_case_split_queue.activity_changed_eh(v, new_act > old_act);
-        }
     }
 
     void solver::set_next_restart() {
@@ -3705,8 +3700,7 @@ namespace sat {
                 if (interval > 0) {
                     auto activity = m_activity[v];
                     auto reward = (m_config.m_reward_offset * (m_participated[v] + m_reasoned[v])) / interval;
-                    m_activity[v] = static_cast<unsigned>(m_step_size * reward + ((1 - m_step_size) * activity));
+                    set_activity(v, static_cast<unsigned>(m_step_size * reward + ((1 - m_step_size) * activity)));
-                    m_case_split_queue.activity_changed_eh(v, m_activity[v] > activity);
                 }
             }
             if (m_config.m_anti_exploration) {
@@ -3968,8 +3962,7 @@ namespace sat {
             auto v = m_trail[i].var();
             auto reward = multiplier / (m_stats.m_conflict - m_last_conflict[v] + 1);            
             auto activity = m_activity[v];
-            m_activity[v] = static_cast<unsigned>(m_step_size * reward + ((1.0 - m_step_size) * activity));
+            set_activity(v, static_cast<unsigned>(m_step_size * reward + ((1.0 - m_step_size) * activity)));
-            m_case_split_queue.activity_changed_eh(v, m_activity[v] > activity);
         }
     }
 

src/smt/smt_context.cpp

@@ -326,6 +326,7 @@ namespace smt {
 
         if (m_manager.has_trace_stream())
             trace_assign(l, j, decision);
+
         m_case_split_queue->assign_lit_eh(l);
 
         // a unit is asserted at search level. Mark it as relevant.
@@ -2005,6 +2006,7 @@ namespace smt {
         SASSERT(m_flushing || !cls->in_reinit_stack());
         if (log) 
             m_clause_proof.del(*cls);
+        CTRACE("context", !m_flushing, display_clause_smt2(tout << "deleting ", *cls) << "\n";);
         if (!cls->deleted())
             remove_cls_occs(cls);
         cls->deallocate(m_manager);
@@ -2549,13 +2551,14 @@ namespace smt {
         for(; it != end; ++it) {
             clause * cls = *it;
             SASSERT(!cls->in_reinit_stack());
-            TRACE("simplify_clauses_bug", display_clause(tout, cls); tout << "\n";);
             
             if (cls->deleted()) {
+                TRACE("simplify_clauses_bug", display_clause(tout << "deleted\n", cls) << "\n";);
                 del_clause(true, cls);
                 num_del_clauses++;
             }
             else if (simplify_clause(*cls)) {
+                TRACE("simplify_clauses_bug", display_clause_smt2(tout << "simplified\n", *cls) << "\n";);
                 for (unsigned idx = 0; idx < 2; idx++) {
                     literal     l0        = (*cls)[idx];
                     b_justification l0_js = get_justification(l0.var());
@@ -3335,6 +3338,33 @@ namespace smt {
         if (r == l_true && get_cancel_flag()) {
             r = l_undef;
         }
+        if (r == l_true && gparams::get_value("model_validate") == "true") {
+            for (theory* t : m_theory_set) {
+                t->validate_model(*m_model);
+            }
+            for (literal lit : m_assigned_literals) {
+                if (!is_relevant(lit)) continue;
+                expr* v = m_bool_var2expr[lit.var()];
+                if (lit.sign() ? m_model->is_true(v) : m_model->is_false(v)) {
+                    IF_VERBOSE(10, verbose_stream() 
+                               << "invalid assignment " << (lit.sign() ? "true" : "false") 
+                               << " to #" << v->get_id() << " := " << mk_bounded_pp(v, m_manager, 1) << "\n");
+                }
+            }
+            for (clause* cls : m_aux_clauses) {
+                bool found = false;
+                for (literal lit : *cls) {
+                    expr* v = m_bool_var2expr[lit.var()];
+                    if (lit.sign() ? !m_model->is_true(v) : !m_model->is_false(v)) {
+                        found = true;
+                        break;
+                    }
+                }
+                if (!found) {
+                    IF_VERBOSE(10, display_clause_smt2(verbose_stream() << "not satisfied:\n", *cls) << "\n");                    
+                }
+            }
+        }
         return r;
     }
 

src/smt/smt_context.h

@@ -1314,6 +1314,10 @@ namespace smt {
             return display_literals(out, lits.size(), lits.c_ptr());
         }
 
+        std::ostream& display_literal_smt2(std::ostream& out, literal lit) const;
+
+        std::ostream& display_literals_smt2(std::ostream& out, unsigned num_lits, literal const* lits) const;
+
         std::ostream& display_literal_verbose(std::ostream & out, literal lit) const;
 
         std::ostream& display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const;
@@ -1326,13 +1330,15 @@ namespace smt {
 
         void display_watch_lists(std::ostream & out) const;
 
-        void display_clause_detail(std::ostream & out, clause const * cls) const;
+        std::ostream& display_clause_detail(std::ostream & out, clause const * cls) const;
 
-        void display_clause(std::ostream & out, clause const * cls) const;
+        std::ostream& display_clause(std::ostream & out, clause const * cls) const;
 
-        void display_clauses(std::ostream & out, ptr_vector<clause> const & v) const;
+        std::ostream& display_clause_smt2(std::ostream & out, clause const& cls) const;
 
-        void display_binary_clauses(std::ostream & out) const;
+        std::ostream& display_clauses(std::ostream & out, ptr_vector<clause> const & v) const;
+
+        std::ostream& display_binary_clauses(std::ostream & out) const;
 
         void display_assignment(std::ostream & out) const;
 

src/smt/smt_context_pp.cpp

@@ -101,12 +101,24 @@ namespace smt {
         display_verbose(out, m_manager, num_lits, lits, m_bool_var2expr.c_ptr(), "\n"); return out;
     }
 
-    void context::display_literal_info(std::ostream & out, literal l) const {
+    std::ostream& context::display_literal_smt2(std::ostream& out, literal l) const {
-        l.display_compact(out, m_bool_var2expr.c_ptr());
         if (l.sign())
             out << "  (not " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << ") ";
         else
             out << "  " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << " ";
+        return out;
+    }
+
+    std::ostream& context::display_literals_smt2(std::ostream& out, unsigned num_lits, literal const* lits) const {
+        for (unsigned i = 0; i < num_lits; ++i) {
+            display_literal_smt2(out, lits[i]) << "\n";
+        }
+        return out;
+    }
+
+    void context::display_literal_info(std::ostream & out, literal l) const {
+        l.display_compact(out, m_bool_var2expr.c_ptr());
+        display_literal_smt2(out, l);
         out << "relevant: " << is_relevant(bool_var2expr(l.var())) << ", val: " << get_assignment(l) << "\n";
     }
 
@@ -144,7 +156,7 @@ namespace smt {
         }
     }
 
-    void context::display_clause_detail(std::ostream & out, clause const * cls) const {
+    std::ostream& context::display_clause_detail(std::ostream & out, clause const * cls) const {
         out << "lemma: " << cls->is_lemma() << "\n";
         for (literal l : *cls) {
             display_literal(out, l);
@@ -152,20 +164,28 @@ namespace smt {
                 << ", ilvl: " << get_intern_level(l.var()) << ", var: " << l.var() << "\n"
                 << mk_pp(bool_var2expr(l.var()), m_manager) << "\n\n";
         }
+        return out;
     }
 
-    void context::display_clause(std::ostream & out, clause const * cls) const {
+    std::ostream& context::display_clause(std::ostream & out, clause const * cls) const {
-        cls->display_smt2(out, m_manager, m_bool_var2expr.c_ptr());
+        cls->display_compact(out, m_manager, m_bool_var2expr.c_ptr());
+        return out;
     }
 
-    void context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const {
+    std::ostream& context::display_clause_smt2(std::ostream & out, clause const& cls) const {
+        cls.display_smt2(out, m_manager, m_bool_var2expr.c_ptr());
+        return out;
+    }
+
+    std::ostream& context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const {
         for (clause* cp : v) {
-            display_clause(out, cp);
+            display_clause_smt2(out, *cp);
             out << "\n";
         }
+        return out;
     }
 
-    void context::display_binary_clauses(std::ostream & out) const {
+    std::ostream& context::display_binary_clauses(std::ostream & out) const {
         bool first = true;
         unsigned l_idx = 0;
         for (watch_list const& wl : m_watches) {
@@ -195,6 +215,7 @@ namespace smt {
                 }
             }
         }
+        return out;
     }
 
     void context::display_assignment(std::ostream & out) const {

src/smt/smt_internalizer.cpp

@@ -1339,7 +1339,8 @@ namespace smt {
         default:
             break;
         }
-        TRACE("mk_clause", tout << "after simplification:\n"; display_literals(tout, num_lits, lits); tout << "\n";);
+        TRACE("mk_clause", tout << "after simplification:\n"; display_literals_verbose(tout, num_lits, lits) << "\n";);
+        TRACE("mk_clause", tout << "after simplification:\n"; display_literals_smt2(tout, num_lits, lits););
         unsigned activity = 0;
         if (activity == 0)
             activity = 1;

src/smt/smt_theory.h

@@ -276,13 +276,11 @@ namespace smt {
 
         // ----------------------------------------------------
         //
-        // Model validation (-vldt flag)
+        // Model validation 
         //
         // ----------------------------------------------------
 
-        virtual bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const {
+        virtual void validate_model(model& mdl) {}
-            return true;
-        }
 
         // ----------------------------------------------------
         //

src/smt/theory_arith.h

@@ -682,8 +682,6 @@ namespace smt {
         void flush_eh() override;
         void reset_eh() override;
         
-        bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const override;
-
         // -----------------------------------
         //
         // bool_var -> atom mapping

src/smt/theory_arith_core.h

@@ -1650,11 +1650,6 @@ namespace smt {
         theory::reset_eh();
     }
 
-    template<typename Ext>
-    bool theory_arith<Ext>::validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const {
-        return true;
-    }
-
     /**
        \brief Compute the value of a base or quasi-base variable using
        the value of the dependent variables.

src/smt/theory_dense_diff_logic.h

@@ -241,8 +241,6 @@ namespace smt {
         
         bool dump_lemmas() const { return m_params.m_arith_dump_lemmas; }
 
-        bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const override;
-
         void display(std::ostream & out) const override;
         virtual void display_atom(std::ostream & out, atom * a) const;
         void collect_statistics(::statistics & st) const override;

src/smt/theory_dense_diff_logic_def.h

@@ -425,11 +425,6 @@ namespace smt {
         theory::reset_eh();
     }
     
-    template<typename Ext>
-    bool theory_dense_diff_logic<Ext>::validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const {
-        return is_true ? m_assignment[v1] == m_assignment[v2] : m_assignment[v1] != m_assignment[v2];
-    }
-
     /**
        \brief Store in results the antecedents that justify that the distance between source and target.
     */

src/smt/theory_diff_logic.h

@@ -308,8 +308,6 @@ namespace smt {
         
         model_value_proc * mk_value(enode * n, model_generator & mg) override;
                 
-        bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const override;
-                
         void display(std::ostream & out) const override;
         
         void collect_statistics(::statistics & st) const override;

src/smt/theory_diff_logic_def.h

@@ -911,12 +911,6 @@ model_value_proc * theory_diff_logic<Ext>::mk_value(enode * n, model_generator &
     return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, m_util.is_int(n->get_owner())));
 }
 
-template<typename Ext>
-bool theory_diff_logic<Ext>::validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const {
-    NOT_IMPLEMENTED_YET();
-    return true;
-}
-
 
 template<typename Ext>
 void theory_diff_logic<Ext>::display(std::ostream & out) const {

src/smt/theory_lra.cpp

@@ -3206,12 +3206,6 @@ public:
         return false;
     }
 
-    bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const {
-        SASSERT(v1 != null_theory_var);
-        SASSERT(v2 != null_theory_var);
-        return (get_value(v1) == get_value(v2)) == is_true;
-    }
-
     // Auxiliary verification utilities.
 
     struct scoped_arith_mode {
@@ -3656,10 +3650,6 @@ bool theory_lra::get_lower(enode* n, rational& r, bool& is_strict) {
 bool theory_lra::get_upper(enode* n, rational& r, bool& is_strict) {
     return m_imp->get_upper(n, r, is_strict);
 }
-
-bool theory_lra::validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const {
-    return m_imp->validate_eq_in_model(v1, v2, is_true);
-}
 void theory_lra::display(std::ostream & out) const {
     m_imp->display(out);
 }

src/smt/theory_lra.h

@@ -86,8 +86,6 @@ namespace smt {
         bool get_lower(enode* n, rational& r, bool& is_strict);
         bool get_upper(enode* n, rational& r, bool& is_strict);
                 
-        bool validate_eq_in_model(theory_var v1, theory_var v2, bool is_true) const override;
-                
         void display(std::ostream & out) const override;
         
         void collect_statistics(::statistics & st) const override;

src/smt/theory_seq.cpp

@@ -89,7 +89,9 @@ Outline:
 
 #include <typeinfo>
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "ast/ast_trail.h"
+#include "ast/for_each_expr.h"
 #include "smt/proto_model/value_factory.h"
 #include "smt/smt_context.h"
 #include "smt/smt_model_generator.h"
@@ -138,6 +140,7 @@ void theory_seq::solution_map::update(expr* e, expr* r, dependency* d) {
     value.first = r;
     value.second = d;
     m_map.insert(e, value);
+    // std::cout << mk_pp(e, m) << " -> " << mk_pp(r, m) << "\n";
     add_trail(INS, e, r, d);
 }
 
@@ -322,6 +325,14 @@ void theory_seq::init(context* ctx) {
 
 #define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(31, verbose_stream() << s << "\n"); }
 
+struct scoped_enable_trace {
+    scoped_enable_trace() {
+        enable_trace("seq");
+    }
+    ~scoped_enable_trace() {
+        disable_trace("seq");
+    }
+};
 
 final_check_status theory_seq::final_check_eh() {
     if (m_reset_cache) {
@@ -402,7 +413,9 @@ final_check_status theory_seq::final_check_eh() {
         return FC_CONTINUE;
     }
     if (is_solved()) {
+        //scoped_enable_trace _se;
         TRACEFIN("is_solved");
+        TRACE("seq", display(tout););
         return FC_DONE;
     }
     TRACEFIN("give_up");
@@ -1024,7 +1037,7 @@ void theory_seq::prop_arith_to_len_offset() {
     }
 }
 
-int theory_seq::find_fst_non_empty_idx(expr_ref_vector const& xs) const {
+int theory_seq::find_fst_non_empty_idx(expr_ref_vector const& xs) {
     context & ctx = get_context();    
     for (unsigned i = 0; i < xs.size(); ++i) {
         expr* x = xs[i];
@@ -1042,7 +1055,7 @@ int theory_seq::find_fst_non_empty_idx(expr_ref_vector const& xs) const {
     return -1;
 }
 
-expr* theory_seq::find_fst_non_empty_var(expr_ref_vector const& x) const {
+expr* theory_seq::find_fst_non_empty_var(expr_ref_vector const& x) {
     int i = find_fst_non_empty_idx(x);
     if (i >= 0)
         return x[i];
@@ -2242,6 +2255,19 @@ bool theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vect
             eqs.push_back(enode_pair(a.n1, a.n2));
         }
     }
+    if (!asserted) {
+        std::cout << "not asserted\n";
+        context& ctx = get_context();
+        for (assumption const& a : assumptions) {
+            if (a.lit != null_literal) {
+                std::cout << a.lit << " " << ctx.get_assignment(a.lit) << " ";
+                ctx.display_literal_info(std::cout, a.lit);
+                ctx.display_detailed_literal(std::cout, a.lit) << "\n";
+            }
+        }
+        // ctx.display(std::cout);
+        exit(0);
+    }
     return asserted;
 }
 
@@ -2308,8 +2334,8 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
         TRACE("seq", tout << "not linearized\n";);
         return;
     }
-    TRACE("seq",
+    TRACE("seq_verbose",
-          tout << "assert: " << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <-\n";
+          tout << "assert: " << mk_bounded_pp(n1->get_owner(), m) << " = " << mk_bounded_pp(n2->get_owner(), m) << " <-\n";
           display_deps(tout, dep); 
           );
 
@@ -2355,15 +2381,44 @@ void theory_seq::enforce_length_coherence(enode* n1, enode* n2) {
 }
 
 
+bool theory_seq::lift_ite(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
+    if (ls.size() != 1 || rs.size() != 1) {
+        return false;
+    }
+    context& ctx = get_context();
+    expr* c = nullptr, *t = nullptr, *e = nullptr;
+    expr* l = ls[0], *r = rs[0];
+    if (m.is_ite(r)) {
+        std::swap(l, r);
+    }
+    if (!m.is_ite(l, c, t, e)) {
+        return false;
+    }
+     
+    switch (ctx.find_assignment(c)) {
+    case l_undef: 
+        return false;
+    case l_true:
+        deps = mk_join(deps, ctx.get_literal(c));
+        m_eqs.push_back(mk_eqdep(t, r, deps));
+        return true;
+    case l_false:
+        deps = mk_join(deps, ~ctx.get_literal(c));
+        m_eqs.push_back(mk_eqdep(e, r, deps));
+        return true;
+    }
+    return false;
+}
+
 
 bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependency* deps) {
     context& ctx = get_context();
     expr_ref_vector lhs(m), rhs(m);
     bool changed = false;
-    TRACE("seq", tout << ls << " = " << rs << "\n";);
+    TRACE("seq_verbose", tout << ls << " = " << rs << "\n";);
     if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, changed)) {
         // equality is inconsistent.
-        TRACE("seq", tout << ls << " != " << rs << "\n";);
+        TRACE("seq_verbose", tout << ls << " != " << rs << "\n";);
         set_conflict(deps);
         return true;
     }
@@ -2377,7 +2432,7 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
         TRACE("seq", tout << "solved\n";);
         return true;
     }
-    TRACE("seq", 
+    TRACE("seq_verbose", 
           tout << ls << " = " << rs << "\n";
           tout << lhs << " = " << rhs << "\n";);
     for (unsigned i = 0; !ctx.inconsistent() && i < lhs.size(); ++i) {
@@ -2394,7 +2449,7 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
             propagate_eq(deps, ensure_enode(li), ensure_enode(ri));
         }
     }
-    TRACE("seq",
+    TRACE("seq_verbose",
           if (!ls.empty() || !rs.empty()) tout << ls << " = " << rs << ";\n";
           for (unsigned i = 0; i < lhs.size(); ++i) {
               tout << mk_pp(lhs.get(i), m) << " = " << mk_pp(rhs.get(i), m) << ";\n";
@@ -2523,6 +2578,7 @@ bool theory_seq::is_var(expr* a) const {
         !m_util.str.is_string(a) &&
         !m_util.str.is_unit(a) &&
         !m_util.str.is_itos(a) &&
+        !m_util.str.is_nth_i(a) && 
         // !m_util.str.is_extract(a) && 
         !m.is_ite(a);
 }
@@ -2560,7 +2616,7 @@ bool theory_seq::solve_eqs(unsigned i) {
             m_eqs.pop_back();
             change = true;
         }
-        TRACE("seq", display_equations(tout););
+        TRACE("seq_verbose", display_equations(tout););
     }
     return change || m_new_propagation || ctx.inconsistent();
 }
@@ -2574,7 +2630,7 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
     bool change = canonize(l, ls, dep2);
     change = canonize(r, rs, dep2) || change;
     deps = m_dm.mk_join(dep2, deps);
-    TRACE("seq", tout << l << " = " << r << " ==> ";
+    TRACE("seq_verbose", tout << l << " = " << r << " ==> ";
           tout << ls << " = " << rs << "\n";
           display_deps(tout, deps);
           );
@@ -2582,7 +2638,10 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
         TRACE("seq", tout << "simplified\n";);
         return true;
     }
-    TRACE("seq", tout << ls << " = " << rs << "\n";);
+    if (!ctx.inconsistent() && lift_ite(ls, rs, deps)) {
+        return true;
+    }
+    TRACE("seq_verbose", tout << ls << " = " << rs << "\n";);
     if (ls.empty() && rs.empty()) {
         return true;
     }
@@ -3526,9 +3585,7 @@ bool theory_seq::internalize_term(app* term) {
     return true;
 }
 
-void theory_seq::add_length(expr* l) {
+void theory_seq::add_length(expr* e, expr* l) {
-    expr* e = nullptr;
-    VERIFY(m_util.str.is_length(l, e));
     SASSERT(!m_length.contains(l));
     m_length.push_back(l);
     m_has_length.insert(e);
@@ -3546,9 +3603,9 @@ void theory_seq::enforce_length(expr* e) {
     do {
         expr* o = n->get_owner();
         if (!has_length(o)) {
-            expr_ref len = mk_len(o);
+            expr_ref len(m_util.str.mk_length(o), m);
             enque_axiom(len);
-            add_length(len);
+            add_length(o, len);
         }
         n = n->get_next();
     }
@@ -4119,6 +4176,54 @@ app* theory_seq::mk_value(app* e) {
 }
 
 
+void theory_seq::validate_model(model& mdl) {
+    std::cout << "validate-seq-model\n";
+    for (auto const& eq : m_eqs) {
+        expr_ref_vector ls = eq.ls();
+        expr_ref_vector rs = eq.rs();
+        expr_ref l(m_util.str.mk_concat(ls), m);
+        expr_ref r(m_util.str.mk_concat(rs), m);
+        if (!mdl.are_equal(l, r)) {
+            IF_VERBOSE(0, verbose_stream() << l << " = " << r << " but " << mdl(l) << " != " << mdl(r) << "\n");
+        }
+    }
+
+    for (auto const& ne : m_nqs) {
+        expr_ref l = ne.l();
+        expr_ref r = ne.r();
+        if (mdl.are_equal(l, r)) {
+            IF_VERBOSE(0, verbose_stream() << l << " = " << r << " = " << mdl(l) << "\n");
+        }
+    }
+
+    for (auto const& ex : m_exclude) {
+        expr_ref l(ex.first, m);
+        expr_ref r(ex.second, m);
+        if (mdl.are_equal(l, r)) {
+            IF_VERBOSE(0, verbose_stream() << "exclude " << l << " = " << r << " = " << mdl(l) << "\n");
+        }
+    }
+
+    for (auto const& nc : m_ncs) {
+        expr_ref p = nc.contains();
+        if (!mdl.is_false(p)) {
+            IF_VERBOSE(0, verbose_stream() << p << " evaluates to " << mdl(p) << "\n");
+        }
+    }
+
+#if 0
+    ptr_vector<expr> fmls;
+    context& ctx = get_context();
+    ctx.get_asserted_formulas(fmls);
+    validate_model_proc proc(*this, mdl);
+    for (expr* f : fmls) {
+        for_each_expr(proc, f);
+    }
+#endif
+}
+
+
+
 theory_var theory_seq::mk_var(enode* n) {
     if (!m_util.is_seq(n->get_owner()) &&
         !m_util.is_re(n->get_owner())) {
@@ -4385,9 +4490,8 @@ void theory_seq::propagate() {
 }
 
 void theory_seq::enque_axiom(expr* e) {
-    TRACE("seq", tout << "enqueue_axiom " << mk_pp(e, m) << " " << m_axiom_set.contains(e) << "\n";);    
     if (!m_axiom_set.contains(e)) {
-        TRACE("seq", tout << "add axiom " << mk_pp(e, m) << "\n";);
+        TRACE("seq", tout << "add axiom " << mk_bounded_pp(e, m) << "\n";);
         m_axioms.push_back(e);
         m_axiom_set.insert(e);
         m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_axioms));
@@ -4436,6 +4540,9 @@ void theory_seq::deque_axiom(expr* n) {
     else if (m_util.str.is_le(n)) {
         add_le_axiom(n);
     }
+    else if (m_util.str.is_unit(n)) {
+        add_unit_axiom(n);
+    }
 }
 
 
@@ -4843,6 +4950,13 @@ expr_ref theory_seq::mk_add(expr* a, expr* b) {
     return result;
 }
 
+expr_ref theory_seq::mk_len(expr* s) {
+    expr_ref result(m_util.str.mk_length(s), m); 
+    m_rewrite(result);
+    return result;
+}
+
+
 enode* theory_seq::ensure_enode(expr* e) {
     context& ctx = get_context();
     if (!ctx.e_internalized(e)) {
@@ -4924,7 +5038,7 @@ bool theory_seq::lower_bound2(expr* _e, rational& lo) {
 }
 
 
-bool theory_seq::get_length(expr* e, rational& val) const {
+bool theory_seq::get_length(expr* e, rational& val) {
     rational val1;
     expr_ref len(m), len_val(m);
     expr* e1 = nullptr, *e2 = nullptr;
@@ -4992,11 +5106,11 @@ this translates to:
 
 */
 
+
 void theory_seq::add_extract_axiom(expr* e) {
     TRACE("seq", tout << mk_pp(e, m) << "\n";);
     expr* s = nullptr, *i = nullptr, *l = nullptr;
     VERIFY(m_util.str.is_extract(e, s, i, l));
-#if 0
     if (is_tail(s, i, l)) {
         add_tail_axiom(e, s);
         return;
@@ -5013,7 +5127,6 @@ void theory_seq::add_extract_axiom(expr* e) {
         add_extract_suffix_axiom(e, s, i);
         return;
     }
-#endif
     expr_ref x(mk_skolem(m_pre, s, i), m);
     expr_ref ls = mk_len(s);
     expr_ref lx = mk_len(x);
@@ -5033,6 +5146,7 @@ void theory_seq::add_extract_axiom(expr* e) {
     literal ls_le_0   = mk_simplified_literal(m_autil.mk_le(ls, zero));
     literal le_is_0   = mk_eq(le, zero, false);
 
+    
     add_axiom(~i_ge_0, ~i_le_ls, mk_seq_eq(xey, s));
     add_axiom(~i_ge_0, ~i_le_ls, mk_eq(lx, i, false));
     add_axiom(~i_ge_0, ~i_le_ls, ~l_ge_0, ~li_ge_ls, mk_eq(le, l, false));
@@ -5156,7 +5270,7 @@ void theory_seq::add_at_axiom(expr* e) {
     literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
 
     rational iv;
-    if (m_autil.is_numeral(i, iv) && iv.is_int() && !iv.is_neg()) {
+    if (m_autil.is_numeral(i, iv) && iv.is_unsigned()) {
         expr_ref_vector es(m);
         expr_ref nth(m);
         unsigned k = iv.get_unsigned();
@@ -5183,6 +5297,12 @@ void theory_seq::add_at_axiom(expr* e) {
     add_axiom(~i_ge_len_s, mk_eq(e, emp, false));
 }
 
+/**
+   \brief
+
+   i >= 0 i < len(s) => unit(nth_i(s, i)) = at(s, i)
+   nth_i(unit(nth_i(s, i)), 0) = nth_i(s, i)
+ */
 void theory_seq::add_nth_axiom(expr* e) {
     expr* s = nullptr, *i = nullptr;
     rational n;
@@ -5198,8 +5318,15 @@ void theory_seq::add_nth_axiom(expr* e) {
         literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
         // at(s,i) = [nth(s,i)]
         expr_ref rhs(s, m);
-        if (!m_util.str.is_at(s)) rhs = m_util.str.mk_at(s, i);
+        expr_ref lhs(m_util.str.mk_unit(e), m);
-        add_axiom(~i_ge_0, i_ge_len_s, mk_eq(m_util.str.mk_unit(e), rhs, false));        
+        if (!m_util.str.is_at(s) || zero != i) rhs = m_util.str.mk_at(s, i);
+        if (e->get_id() == 420) {
+            enable_trace("seq");
+        }
+        add_axiom(~i_ge_0, i_ge_len_s, mk_eq(lhs, rhs, false));
+        if (e->get_id() == 420) {
+            disable_trace("seq");
+        }        
     }
 }
 
@@ -5308,7 +5435,14 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
         log_axiom_instantiation(body);
     }
     ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
-    if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+    if (m.has_trace_stream()) {
+        m.trace_stream() << "[end-of-instance]\n";
+    }
+
+    if (!ctx.at_base_level() && l2 == null_literal) {
+        m_trail_stack.push(push_replay(alloc(replay_unit_literal, m, ctx.bool_var2expr(l1.var()), l1.sign())));
+        
+    }
 }
 
 
@@ -5449,14 +5583,13 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     expr* e1 = nullptr, *e2 = nullptr;
     expr_ref f(m);
     literal lit(v, !is_true);
+    TRACE("seq", tout << (is_true?"":"not ") << mk_pp(e, m) << "\n";);
 
     if (m_util.str.is_prefix(e, e1, e2)) {
         if (is_true) {
             f = mk_skolem(m_prefix, e1, e2);
             f = mk_concat(e1, f);
             propagate_eq(lit, f, e2, true);
-            //literal len1_le_len2 = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(e2), mk_len(e1)), m_autil.mk_int(0)));
-            //add_axiom(~lit, len1_le_len2);
         }
         else {
             propagate_not_prefix(e);
@@ -5467,8 +5600,6 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             f = mk_skolem(m_suffix, e1, e2);
             f = mk_concat(f, e1);
             propagate_eq(lit, f, e2, true);
-            //literal len1_le_len2 = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(e2), mk_len(e1)), m_autil.mk_int(0)));
-            //add_axiom(~lit, len1_le_len2);
         }
         else {
             propagate_not_suffix(e);
@@ -5580,7 +5711,7 @@ lbool theory_seq::regex_are_equal(expr* r1, expr* r2) {
 
 
 void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
-    TRACE("seq", tout << expr_ref(n1->get_owner(), m) << " = " << expr_ref(n2->get_owner(), m) << "\n";);
+    TRACE("seq", tout << mk_bounded_pp(n1->get_owner(), m) << " = " << mk_bounded_pp(n2->get_owner(), m) << "\n";);
     if (n1 != n2 && m_util.is_seq(n1->get_owner())) {
         theory_var v1 = n1->get_th_var(get_id());
         theory_var v2 = n2->get_th_var(get_id());
@@ -5590,7 +5721,7 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
         m_find.merge(v1, v2);
         expr_ref o1(n1->get_owner(), m);
         expr_ref o2(n2->get_owner(), m);
-        TRACE("seq", tout << o1 << " = " << o2 << "\n";);
+        TRACE("seq", tout << mk_bounded_pp(o1, m) << " = " << mk_bounded_pp(o2, m) << "\n";);
         m_eqs.push_back(mk_eqdep(o1, o2, deps));
         solve_eqs(m_eqs.size()-1);
         enforce_length_coherence(n1, n2);
@@ -5651,15 +5782,17 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
     m_rewrite(eq);
     if (!m.is_false(eq)) {
         literal lit = mk_eq(e1, e2, false);
-
+        get_context().mark_as_relevant(lit);
         if (m_util.str.is_empty(e2)) {
             std::swap(e1, e2);
         }
 
         dependency* dep = m_dm.mk_leaf(assumption(~lit));
         m_nqs.push_back(ne(e1, e2, dep));
+        if (get_context().get_assignment(lit) != l_undef) {
             solve_nqs(m_nqs.size() - 1);
         }
+    }
 }
 
 void theory_seq::push_scope_eh() {
@@ -5700,6 +5833,7 @@ void theory_seq::restart_eh() {
 }
 
 void theory_seq::relevant_eh(app* n) {
+    TRACE("seq", tout << mk_pp(n, m) << "\n";);
     if (m_util.str.is_index(n)   ||
         m_util.str.is_replace(n) ||
         m_util.str.is_extract(n) ||
@@ -5710,6 +5844,7 @@ void theory_seq::relevant_eh(app* n) {
         m_util.str.is_itos(n) || 
         m_util.str.is_stoi(n) ||
         m_util.str.is_lt(n) ||
+        m_util.str.is_unit(n) ||
         m_util.str.is_le(n)) {
         enque_axiom(n);
     }
@@ -5922,9 +6057,6 @@ void theory_seq::propagate_not_prefix(expr* e) {
     VERIFY(m_util.str.is_prefix(e, e1, e2));
     literal lit = ctx.get_literal(e);
     SASSERT(ctx.get_assignment(lit) == l_false);
-    if (canonizes(false, e)) {
-        return;
-    }
     propagate_non_empty(~lit, e1);
     literal e1_gt_e2 = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(e1), mk_len(e2)), m_autil.mk_int(1)));
     sort* char_sort = nullptr;
@@ -5951,9 +6083,6 @@ void theory_seq::propagate_not_suffix(expr* e) {
     VERIFY(m_util.str.is_suffix(e, e1, e2));
     literal lit = ctx.get_literal(e);
     SASSERT(ctx.get_assignment(lit) == l_false);
-    if (canonizes(false, e)) {
-        return;
-    }
     propagate_non_empty(~lit, e1);
     literal e1_gt_e2 = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(e1), mk_len(e2)), m_autil.mk_int(1)));    
     sort* char_sort = nullptr;
@@ -5968,6 +6097,14 @@ void theory_seq::propagate_not_suffix(expr* e) {
     add_axiom(lit, e1_gt_e2, ~mk_eq(c, d, false));
 }
 
+void theory_seq::add_unit_axiom(expr* n) {
+    expr* u = nullptr;
+    VERIFY(m_util.str.is_unit(n, u));
+    sort* s = m.get_sort(u);
+    expr_ref rhs(mk_skolem(symbol("inv-unit"), n, nullptr, nullptr, nullptr, s), m);
+    add_axiom(mk_eq(u, rhs, false));
+}
+
 /**
    e1 < e2 => e1 = empty or e1 = xcy
    e1 < e2 => e1 = empty or c < d

src/smt/theory_seq.h

@@ -50,6 +50,7 @@ namespace smt {
         typedef union_find<theory_seq> th_union_find;
 
         class seq_value_proc;
+        struct validate_model_proc;
         
         // cache to track evaluations under equalities
         class eval_cache {
@@ -97,7 +98,9 @@ namespace smt {
 
         // Table of current disequalities
         class exclusion_table {
+        public:
             typedef obj_pair_hashtable<expr, expr> table_t;
+        protected:
             ast_manager&                      m;
             table_t                           m_table;
             expr_ref_vector                   m_lhs, m_rhs;
@@ -111,6 +114,8 @@ namespace smt {
             void push_scope() { m_limit.push_back(m_lhs.size()); }
             void pop_scope(unsigned num_scopes);
             void display(std::ostream& out) const;            
+            table_t::iterator begin() const { return m_table.begin(); }
+            table_t::iterator end() const { return m_table.end(); }
         };
 
         // Asserted or derived equality with dependencies
@@ -260,6 +265,20 @@ namespace smt {
             }
         };
 
+        class replay_unit_literal : public apply {
+            bool     m_sign;
+            expr_ref m_e;
+        public:
+            replay_unit_literal(ast_manager& m, expr* e, bool sign) : m_e(e, m), m_sign(sign) {}
+            ~replay_unit_literal() override {}
+            void operator()(theory_seq& th) override {
+                literal lit = th.mk_literal(m_e);
+                if (m_sign) lit.neg();
+                th.add_axiom(lit);
+                m_e.reset();
+            }
+
+        };
 
         class replay_is_axiom : public apply {
             expr_ref m_e;
@@ -290,6 +309,7 @@ namespace smt {
             }
         };
 
+
         struct s_in_re {
             literal     m_lit;
             expr*       m_s;
@@ -404,6 +424,7 @@ namespace smt {
         void init_model(model_generator & mg) override;
         void finalize_model(model_generator & mg) override;
         void init_search_eh() override;
+        void validate_model(model& mdl) override;
 
         void init_model(expr_ref_vector const& es);
         app* get_ite_value(expr* a);
@@ -411,8 +432,8 @@ namespace smt {
         
         void len_offset(expr* e, rational val);
         void prop_arith_to_len_offset();
-        int find_fst_non_empty_idx(expr_ref_vector const& x) const;
+        int find_fst_non_empty_idx(expr_ref_vector const& x);
-        expr* find_fst_non_empty_var(expr_ref_vector const& x) const;
+        expr* find_fst_non_empty_var(expr_ref_vector const& x);
         void find_max_eq_len(expr_ref_vector const& ls, expr_ref_vector const& rs);
         bool has_len_offset(expr_ref_vector const& ls, expr_ref_vector const& rs, int & diff);
         bool find_better_rep(expr_ref_vector const& ls, expr_ref_vector const& rs, unsigned idx, dependency*& deps, expr_ref_vector & res);
@@ -462,6 +483,7 @@ namespace smt {
         bool solve_eqs(unsigned start);
         bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep, unsigned idx);
         bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
+        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);
@@ -566,7 +588,7 @@ namespace smt {
         
 
         bool has_length(expr *e) const { return m_has_length.contains(e); }
-        void add_length(expr* e);
+        void add_length(expr* e, expr* l);
         void enforce_length(expr* n);
         bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
         void enforce_length_coherence(enode* n1, enode* n2);
@@ -580,6 +602,7 @@ namespace smt {
         void add_at_axiom(expr* n);
         void add_lt_axiom(expr* n);
         void add_le_axiom(expr* n);
+        void add_unit_axiom(expr* n);
         void add_nth_axiom(expr* n);
         void add_in_re_axiom(expr* n);
         void add_itos_axiom(expr* n);
@@ -599,7 +622,7 @@ namespace smt {
         void tightest_prefix(expr* s, expr* x);
         expr_ref mk_sub(expr* a, expr* b);
         expr_ref mk_add(expr* a, expr* b);
-        expr_ref mk_len(expr* s) const { return expr_ref(m_util.str.mk_length(s), m); }
+        expr_ref mk_len(expr* s);
         enode* ensure_enode(expr* a);
         enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }
         dependency* mk_join(dependency* deps, literal lit);
@@ -611,7 +634,7 @@ namespace smt {
         bool lower_bound(expr* s, rational& lo) const;
         bool lower_bound2(expr* s, rational& lo);
         bool upper_bound(expr* s, rational& hi) const;
-        bool get_length(expr* s, rational& val) const;
+        bool get_length(expr* s, rational& val);
 
         void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
         expr_ref coalesce_chars(expr* const& str);

src/smt/theory_utvpi.h

@@ -251,10 +251,6 @@ namespace smt {
         
         model_value_proc * mk_value(enode * n, model_generator & mg) override;
                 
-        bool validate_eq_in_model(th_var v1, th_var v2, bool is_true) const override {
-            return true;
-        }
-                
         void display(std::ostream & out) const override;
         
         void collect_statistics(::statistics & st) const override;