diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 789aaf8db..25b51372e 100644
--- a/src/opt/maxres.cpp
+++ b/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););
- VERIFY(is_sat == l_false);
+ _solver->display(tout);
+ tout << "other solver\n";
+ s().display(tout);
+ );
+ VERIFY(is_sat == l_false || m.canceled());
}
void verify_assumptions() {
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 7fdfbf9aa..9a3ae7728 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/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()))
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 6f382a5f6..ef018b895 100644
--- a/src/smt/smt_context.h
+++ b/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;
// -----------------------------------
//
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 72cc2404c..c40b829a7 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/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 (unsigned i = 0; i < sz; i++)
- out << mk_pp(m_unsat_core.get(i), m_manager) << "\n";
+ for (expr* c : m_unsat_core) {
+ out << mk_pp(c, 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++)
- todo.push_back(to_app(n)->get_arg(i));
+ for (expr* arg : *to_app(n)) {
+ 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 {
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 86d84c60a..875fe8de4 100644
--- a/src/smt/theory_pb.cpp
+++ b/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
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 2864182eb..37297997a 100644
--- a/src/smt/theory_seq.cpp
+++ b/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 =>
- // len(tail(s, l)) = len(s) - l - 1
+ // e = tail(s, l), len(s) > l => 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)) {