From 841c48e04df40c0b91f7eabfbdc32b3a80173891 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Nov 2017 18:24:45 -0800 Subject: [PATCH] fix break Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 1286fa85d..fb8f36c59 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3230,8 +3230,8 @@ void theory_seq::add_indexof_axiom(expr* i) { // offset > len(t) => indexof(t, s, offset) = -1 // offset = len(t) & |s| = 0 => indexof(t, s, offset) = offset expr_ref len_t(m_util.str.mk_length(t), m); - literal offset_ge_len = mk_simplified_literal(m_autil.mk_ge(offset, len_t)); - literal offset_le_len = mk_simplified_literal(m_autil.mk_le(offset, len_t)); + literal offset_ge_len = mk_simplified_literal(m_autil.mk_ge(m_autil.mk_sub(offset, len_t), zero)); + literal offset_le_len = mk_simplified_literal(m_autil.mk_le(m_autil.mk_sub(offset, len_t), zero)); literal i_eq_offset = mk_eq(i, offset, false); add_axiom(~offset_ge_len, s_eq_empty, i_eq_m1); add_axiom(offset_le_len, i_eq_m1);