From 611314913895c4fca80dde62c07c1fb4d2eddc59 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Jan 2019 20:20:34 -0800 Subject: [PATCH] fix #2060. Code comment was right, code wasn't. Code comment and code could also be tuned Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index e384c7b1f..c3274d7ab 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3536,7 +3536,7 @@ expr_ref theory_seq::digit2int(expr* ch) { -// n >= 0 & len(e) = k => is_digit(e_i) for i = 0..k-1 +// n >= 0 & len(e) >= i + 1 => is_digit(e_i) for i = 0..k-1 // n >= 0 & len(e) = k => n = sum 10^i*digit(e_i) // n < 0 & len(e) = k => \/_i ~is_digit(e_i) for i = 0..k-1 // 10^k <= n < 10^{k+1}-1 => len(e) = k @@ -3556,7 +3556,9 @@ void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) { for (unsigned i = 0; i < k; ++i) { ith_char = mk_nth(e, m_autil.mk_int(i)); literal isd = is_digit(ith_char); - add_axiom(~len_eq_k, ~ge0, isd); + literal len_ge_i1 = mk_literal(m_autil.mk_ge(len, m_autil.mk_int(i+1))); + add_axiom(~len_ge_i1, ~ge0, isd); + digits.push_back(~isd); chars.push_back(m_util.str.mk_unit(ith_char)); nums.push_back(digit2int(ith_char)); }