From 4cefa524970988d97e4b1e8e0abe6195dcf09d5b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 28 Jun 2026 17:16:46 -0700
Subject: [PATCH] tweaks to string solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_axioms.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index fa77f0d7f6..5d38ca2ddb 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -446,6 +446,8 @@ namespace seq {
         // |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
         // ~contains(t,s) => indexof(t,s,offset) = -1
 
+        add_clause(mk_ge(i, -1));
+
         add_clause(cnt,  i_eq_m1);
         add_clause(~t_eq_empty, s_eq_empty, i_eq_m1);