From 334e6da60d76c2c36374515d5fb226bcbab8eeca Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 10 Mar 2026 20:14:53 +0000
Subject: [PATCH] Guard mod constraint: skip for period <= 1

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/theory_seq_len.cpp | 34 +++++++++++++++++++---------------
 1 file changed, 19 insertions(+), 15 deletions(-)

diff --git a/src/smt/theory_seq_len.cpp b/src/smt/theory_seq_len.cpp
index affe4780b..4eb50fd7b 100644
--- a/src/smt/theory_seq_len.cpp
+++ b/src/smt/theory_seq_len.cpp
@@ -331,7 +331,7 @@ namespace smt {
             // Semi-linear: lengths are {base + k * period : k >= 0}
             // Assert:
             //   (s in R) => |s| >= base
-            //   (s in R) => |s| mod period = base mod period
+            //   (s in R) => |s| mod period = base mod period  (only when period >= 2)
 
             // |s| >= base
             expr_ref ge_base(m_autil.mk_ge(len, m_autil.mk_int(base)), m);
@@ -347,22 +347,26 @@ namespace smt {
             }
 
             // |s| mod period = base mod period
-            expr_ref mod_len(m_autil.mk_mod(len, m_autil.mk_int(period)), m);
-            expr_ref eq_mod(m.mk_eq(mod_len, m_autil.mk_int(base % period)), m);
-            if (!ctx.b_internalized(eq_mod))
-                ctx.internalize(eq_mod, true);
-            literal eq_mod_lit = ctx.get_literal(eq_mod);
-            ctx.mark_as_relevant(eq_mod_lit);
-            {
-                literal_vector lits;
-                lits.push_back(~lit);
-                lits.push_back(eq_mod_lit);
-                assert_axiom(lits);
+            // Skip when period <= 1: period == 0 is already handled above;
+            // period == 1 makes the constraint trivially true (n mod 1 = 0).
+            if (period >= 2) {
+                expr_ref mod_len(m_autil.mk_mod(len, m_autil.mk_int(period)), m);
+                expr_ref eq_mod(m.mk_eq(mod_len, m_autil.mk_int(base % period)), m);
+                if (!ctx.b_internalized(eq_mod))
+                    ctx.internalize(eq_mod, true);
+                literal eq_mod_lit = ctx.get_literal(eq_mod);
+                ctx.mark_as_relevant(eq_mod_lit);
+                {
+                    literal_vector lits;
+                    lits.push_back(~lit);
+                    lits.push_back(eq_mod_lit);
+                    assert_axiom(lits);
+                }
             }
 
-            TRACE(seq, tout << "seq_len: (s in R) => |s| >= " << base << " && |s| mod "
-                            << period << " = " << (base % period) << " for s=" << mk_pp(s, m)
-                            << " r=" << mk_pp(r, m) << "\n";);
+            TRACE(seq, tout << "seq_len: (s in R) => |s| >= " << base
+                            << (period >= 2 ? " && |s| mod " + std::to_string(period) + " = " + std::to_string(base % period) : "")
+                            << " for s=" << mk_pp(s, m) << " r=" << mk_pp(r, m) << "\n";);
         }
     }