From acba529bce28d98204c95bb6493a9de45478ff12 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2016 15:32:15 +0100 Subject: [PATCH] fix bug in encoding of axioms for indexof. Issue #806 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 245ffe438..3be3fd5f8 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2916,7 +2916,7 @@ void theory_seq::add_indexof_axiom(expr* i) { expr_ref len_t(m_util.str.mk_length(t), m); literal offset_ge_len = mk_literal(m_autil.mk_ge(mk_sub(offset, len_t), zero)); - add_axiom(offset_ge_len, mk_eq(i, minus_one, false)); + add_axiom(~offset_ge_len, mk_eq(i, minus_one, false)); expr_ref x = mk_skolem(m_indexof_left, t, s, offset); expr_ref y = mk_skolem(m_indexof_right, t, s, offset);