From ad2934f8cf5cdd2abdeb3a8417aeec1edacb7f3a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Jul 2025 15:38:25 -0700 Subject: [PATCH] fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index b7c0b7186..22114aecc 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -1243,7 +1243,7 @@ namespace seq { else if (seq.str.is_extract(x, y, offs, l)) { // len(extract(y, o, l)) = l if len(y) >= o + l, o >= 0, l >= 0 // len(extract(y, o, l)) = 0 if o < 0 or l <= 0 or len(y) < o - // len(extract(y, o, l)) = o + l - len(y) if o <= len(y) < o + l + // len(extract(y, o, l)) = len(y) - o if o <= len(y) < o + l expr_ref len_y(mk_len(y), m); expr_ref z(a.mk_int(0), m); expr_ref y_ge_l = mk_ge(a.mk_sub(len_y, a.mk_add(offs, l)), 0); @@ -1255,7 +1255,7 @@ namespace seq { add_clause(offs_ge_0, mk_eq(n, z)); add_clause(l_ge_0, mk_eq(n, z)); add_clause(y_ge_o, mk_eq(n, z)); - add_clause(~y_ge_o, y_ge_l, mk_eq(n, a.mk_sub(a.mk_add(offs, l), len_y))); + add_clause(~y_ge_o, y_ge_l, mk_eq(n, a.mk_sub(len_y, offs))); } else if (seq.str.is_unit(x) || seq.str.is_empty(x) ||