mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

removing axiom exposing unsoundness, replace by weaker axiom

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-01 19:44:16 -08:00
parent f0a30ded7d
commit c1c1b7378c
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_seq.cpp
View file

@ -3221,7 +3221,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
// ~contains(t,s) <=> indexof(t,s,offset) = -1 // ~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(~cnt, ~i_eq_m1);
add_axiom(~t_eq_empty, s_eq_empty, 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())) { 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(~s_eq_empty, i_eq_0);
add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy)); 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, s_eq_empty, mk_eq(i, lenx, false));
add_axiom(~cnt, mk_literal(m_autil.mk_ge(i, zero)));
tightest_prefix(s, x); tightest_prefix(s, x);
} }
else { else {