From 57ede4cdcda1993291965bb12aa9f1f58b60209e Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 10 Mar 2026 23:29:15 +0000
Subject: [PATCH] Address code review: clarify add_lower/upper_int_bound return
 semantics; fix test assertion

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/seq/seq_nielsen.h | 12 ++++++++----
 src/test/seq_nielsen.cpp  |  2 +-
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index c89e74cf6..1660be312 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -540,15 +540,19 @@ namespace seq {
 
         // IntBounds: tighten the lower bound for len(var).
         // Returns true if the bound was tightened (lb > current lower bound).
-        // When tightened, adds an int_constraint len(var) >= lb to this node.
-        // Sets arithmetic conflict if lb > current upper bound.
+        // When tightened without conflict, adds an int_constraint len(var) >= lb.
+        // When lb > current upper bound, sets arithmetic conflict (no constraint added)
+        // and still returns true (the bound value changed). Check is_general_conflict()
+        // separately to distinguish tightening-with-conflict from normal tightening.
         // Mirrors ZIPT's AddLowerIntBound().
         bool add_lower_int_bound(euf::snode* var, unsigned lb, dep_tracker const& dep);
 
         // IntBounds: tighten the upper bound for len(var).
         // Returns true if the bound was tightened (ub < current upper bound).
-        // When tightened, adds an int_constraint len(var) <= ub to this node.
-        // Sets arithmetic conflict if current lower bound > ub.
+        // When tightened without conflict, adds an int_constraint len(var) <= ub.
+        // When current lower bound > ub, sets arithmetic conflict (no constraint added)
+        // and still returns true (the bound value changed). Check is_general_conflict()
+        // separately to distinguish tightening-with-conflict from normal tightening.
         // Mirrors ZIPT's AddHigherIntBound().
         bool add_upper_int_bound(euf::snode* var, unsigned ub, dep_tracker const& dep);
 
diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index bcc3e7faf..c0d58fdd2 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -3477,7 +3477,7 @@ static void test_assert_root_constraints_once() {
     // we can verify the count is stable between iterations by checking
     // that the same constraints weren't added multiple times.
     // The simplest check: count > 0 (constraints were asserted)
-    SASSERT(count_first >= 0);  // at least some constraints asserted
+    SASSERT(count_first > 0);  // x=y produces at least len(x)=len(y) and non-neg constraints
     std::cout << "  asserted " << count_first << " constraints total during solve\n";
     std::cout << "  ok\n";
 }