From 979fd5c6373438cc76a9f5868534bce3d0e351f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Aug 2026 18:13:35 -0700 Subject: [PATCH] Update seq_axioms.cpp --- src/ast/rewriter/seq_axioms.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 404884aac4..031a5a76ac 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -1309,7 +1309,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(len_y, offs))); + add_clause(~offs_ge_0, ~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) ||