From c1c1b7378cffe3ac0781d4765fd1602c40531d33 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Jan 2018 19:44:16 -0800 Subject: [PATCH] removing axiom exposing unsoundness, replace by weaker axiom Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 27ed95155..f91685d43 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3221,7 +3221,7 @@ void theory_seq::add_indexof_axiom(expr* i) { // ~contains(t,s) <=> indexof(t,s,offset) = -1 add_axiom(cnt, i_eq_m1); - add_axiom(~cnt, ~i_eq_m1); +// add_axiom(~cnt, ~i_eq_m1); add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1); if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) { @@ -3234,6 +3234,7 @@ void theory_seq::add_indexof_axiom(expr* i) { add_axiom(~s_eq_empty, i_eq_0); add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy)); add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false)); + add_axiom(~cnt, mk_literal(m_autil.mk_ge(i, zero))); tightest_prefix(s, x); } else {