fix fourth bug produced by repros by Mark Dunlop

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

src/opt/maxres.cpp

@@ -375,7 +375,7 @@ public:
             get_mus_model(mdl);
             is_sat = minimize_core(_core);
             core.append(_core.size(), _core.c_ptr());
-            verify_core(core);
+            DEBUG_CODE(verify_core(core););
             ++m_stats.m_num_cores;
             if (is_sat != l_true) {
                 IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";);
@@ -738,7 +738,7 @@ public:
             m_correction_set_size = correction_set_size;
         }
 
-        TRACE("opt", tout << *mdl;);
+        TRACE("opt_verbose", tout << *mdl;);
 
         rational upper(0);
 
@@ -761,7 +761,7 @@ public:
         m_model = mdl;
         m_c.model_updated(mdl.get());
 
-        TRACE("opt", tout << "updated upper: " << upper << "\nmodel\n" << *m_model;);
+        TRACE("opt", tout << "updated upper: " << upper << "\n";);
 
         for (soft& s : m_soft) {
             s.set_value(m_model->is_true(s.s));
@@ -838,16 +838,17 @@ public:
 
     void commit_assignment() override {
         if (m_found_feasible_optimum) {
-            TRACE("opt", tout << "Committing feasible solution\ndefs:" << m_defs << "\nasms:" << m_asms << "\n";);
             add(m_defs);
             add(m_asms);
+            TRACE("opt", tout << "Committing feasible solution\ndefs:" << m_defs << "\nasms:" << m_asms << "\n";);
+
         }
         // else: there is only a single assignment to these soft constraints.
     }
 
     void verify_core(exprs const& core) {
         return;
-        IF_VERBOSE(3, verbose_stream() << "verify core " << s().check_sat(core.size(), core.c_ptr()) << "\n";);                
+        IF_VERBOSE(1, verbose_stream() << "verify core " << s().check_sat(core.size(), core.c_ptr()) << "\n";);                
         ref<solver> _solver = mk_smt_solver(m, m_params, symbol());
         _solver->assert_expr(s().get_assertions());
         _solver->assert_expr(core);
@@ -855,8 +856,11 @@ public:
         IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << " core size " << core.size() << "\n");
         CTRACE("opt", is_sat != l_false, 
                for (expr* c : core) tout << "core: " << mk_pp(c, m) << "\n";
-               _solver->display(tout););
+               _solver->display(tout);
-        VERIFY(is_sat == l_false);
+               tout << "other solver\n";
+               s().display(tout);
+               );
+        VERIFY(is_sat == l_false || m.canceled());
     }
 
     void verify_assumptions() {

src/smt/smt_conflict_resolution.cpp

@@ -1372,7 +1372,7 @@ namespace smt {
         }
 
         while (true) {
-            TRACE("unsat_core_bug", tout << consequent << " js.get_kind(): " << js.get_kind() << ", idx: " << idx << "\n";);
+            TRACE("unsat_core_bug", tout << consequent << ", idx: " << idx << " " << js.get_kind() << "\n";);
             switch (js.get_kind()) {
             case b_justification::CLAUSE: {
                 clause * cls = js.get_clause();
@@ -1417,7 +1417,7 @@ namespace smt {
             }
             while (idx >= 0) {
                 literal l = m_assigned_literals[idx];
-                TRACE("unsat_core_bug", tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << ", is_marked(l): " << m_ctx.is_marked(l.var()) << "\n";);
+                CTRACE("unsat_core_bug", m_ctx.is_marked(l.var()), tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << "\n";);
                 if (m_ctx.get_assign_level(l) < search_lvl)
                     goto end_unsat_core;
                 if (m_ctx.is_marked(l.var()))

src/smt/smt_context.h

@@ -1358,7 +1358,7 @@ namespace smt {
 
         void display_profile(std::ostream & out) const;
 
-        void display(std::ostream& out, b_justification j) const;
+        std::ostream& display(std::ostream& out, b_justification j) const;
 
         // -----------------------------------
         //

src/smt/smt_context_pp.cpp

@@ -356,9 +356,9 @@ namespace smt {
     }
 
     void context::display_unsat_core(std::ostream & out) const {
-        unsigned sz = m_unsat_core.size();
+        for (expr* c : m_unsat_core) {
-        for (unsigned i = 0; i < sz; i++)
+            out << mk_pp(c, m_manager) << "\n";
-            out << mk_pp(m_unsat_core.get(i), m_manager) << "\n";
+        }
     }
 
     void context::collect_statistics(::statistics & st) const {
@@ -563,13 +563,14 @@ namespace smt {
             }
             out << "\n";
             if (is_app(n)) {
-                for (unsigned i = 0; i < to_app(n)->get_num_args(); i++)
+                for (expr* arg : *to_app(n)) {
-                    todo.push_back(to_app(n)->get_arg(i));
+                    todo.push_back(arg);
+                }
             }
         }
     }
 
-    void context::display(std::ostream& out, b_justification j) const {
+    std::ostream& context::display(std::ostream& out, b_justification j) const {
         switch (j.get_kind()) {
         case b_justification::AXIOM:
             out << "axiom";
@@ -593,7 +594,7 @@ namespace smt {
             UNREACHABLE();
             break;
         }
-        out << "\n";
+        return out << "\n";
     }
 
     void context::trace_assign(literal l, b_justification j, bool decision) const {

src/smt/theory_pb.cpp

@@ -1924,6 +1924,7 @@ namespace smt {
                 process_antecedent(~js.get_literal(), offset);
                 break;
             case b_justification::AXIOM:
+                bound = 0;
                 break;
             case b_justification::JUSTIFICATION: {
                 justification* j = js.get_justification(); 
@@ -1934,6 +1935,7 @@ namespace smt {
                 }
                 if (pbj == nullptr) {
                     TRACE("pb", tout << "skip justification for " << conseq << "\n";);
+                    bound = 0;
                     // this is possible when conseq is an assumption.
                     // The justification of conseq is itself, 
                     // don't increment the cofficient here because it assumes

src/smt/theory_seq.cpp

@@ -2905,17 +2905,26 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
         TRACE("seq", ctx.display_literals_verbose(tout, 2, _lits); tout << "\n";);
     }
     else if (is_skolem(m_tail, e)) {
-        // e = tail(s, l), len(s) > l => 
+        // e = tail(s, l), len(s) > l => len(tail(s, l)) = len(s) - l - 1
-        // len(tail(s, l)) = len(s) - l - 1
+        // e = tail(s, l), len(s) <= l => len(tail(s, l)) = 0
+
         s = to_app(e)->get_arg(0);
         l = to_app(e)->get_arg(1);
         expr_ref len_s = mk_len(s);
         literal len_s_gt_l = mk_simplified_literal(m_autil.mk_ge(mk_sub(len_s, l), m_autil.mk_int(1)));
-        if (ctx.get_assignment(len_s_gt_l) == l_true) {
+        switch (ctx.get_assignment(len_s_gt_l)) {
+        case l_true:
             len = mk_sub(len_s, mk_sub(l, m_autil.mk_int(1)));
             TRACE("seq", tout << len_s << " " << len << " " << len_s_gt_l << "\n";);
             lits.push_back(len_s_gt_l);
             return true;
+        case l_false:
+            len = m_autil.mk_int(0);
+            TRACE("seq", tout << len_s << " " << len << " " << len_s_gt_l << "\n";);
+            lits.push_back(~len_s_gt_l);
+            return true;
+        default:
+            break;
         }
     }
     else if (m_util.str.is_unit(e)) {