From d5cf8e6263837c4862d4ec0ea46603a5fc99d768 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Jun 2026 17:16:30 -0700 Subject: [PATCH] tweaks to string solver Signed-off-by: Nikolaj Bjorner --- src/smt/seq_eq_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index e368e137bd..03cdd6c703 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -189,7 +189,7 @@ bool theory_seq::len_based_split(depeq const& e) { expr_ref_vector const& rs = e.rs; int offset = 0; - if (!has_len_offset(ls, rs, offset)) + if (!has_len_offset(ls, rs, offset) || offset == 0) return false; TRACE(seq, tout << "split based on length\n";);