From e3e6959b70c8b6f85b4465dfc982bf15a2d7791b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Apr 2020 23:30:37 -0700 Subject: [PATCH] fix #4026 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_diff_logic_def.h | 2 -- src/smt/theory_seq.cpp | 3 ++- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 3c64c75ce..d42736735 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -528,9 +528,7 @@ void theory_diff_logic::propagate() { break; } default: - std::cout << m_params.m_arith_propagation_strategy << "\n"; SASSERT(false); - UNREACHABLE(); propagate_core(); } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 93a01e95c..4b1d7e543 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -979,7 +979,7 @@ bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep) literal lit = mk_simplified_literal(m_autil.mk_le(n, m_autil.mk_int(-1))); propagate_lit(dep, 0, nullptr, lit); return true; - } + } expr_ref num(m), digit(m); expr* u = nullptr; for (expr* r : rs) { @@ -992,6 +992,7 @@ bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep) else { num = m_autil.mk_add(m_autil.mk_mul(m_autil.mk_int(10), num), digit); } + propagate_lit(dep, 0, nullptr, m_ax.is_digit(u)); } propagate_lit(dep, 0, nullptr, mk_simplified_literal(m.mk_eq(n, num))); if (rs.size() > 1) {