From 90070fda959c5bd17291abebf7dc768735969cbb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Nov 2018 20:17:09 -0800 Subject: [PATCH] fix #1959 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a4537837b..ccebe0358 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -4823,6 +4823,7 @@ void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) { /* 0 <= i <= len(s) => s = xe & i = len(x) i < 0 => len(e) = 0 + i > len(s) => len(e) = 0 */ void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) { expr_ref x(mk_skolem(m_pre, s, i), m); @@ -4830,11 +4831,13 @@ void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) { expr_ref ls(m_util.str.mk_length(s), m); expr_ref zero(m_autil.mk_int(0), m); expr_ref xe = mk_concat(x, e); + literal le_is_0 = mk_eq(zero, m_util.str.mk_length(e), false); literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero)); literal i_le_s = mk_simplified_literal(m_autil.mk_le(mk_sub(i, ls), zero)); add_axiom(~i_ge_0, ~i_le_s, mk_seq_eq(s, xe)); add_axiom(~i_ge_0, ~i_le_s, mk_eq(i, lx, false)); - add_axiom(i_ge_0, mk_eq(zero, m_util.str.mk_length(e), false)); + add_axiom(i_ge_0, le_is_0); + add_axiom(i_le_s, le_is_0); }