Initialize loop variable `i` before the for loop in abbreviate_atoms
function to fix pyright static type checker error. The previous code
left `i` potentially unbound in edge cases where the range could be
empty, though this would not occur in practice since the loop always
executes at least once with the given range parameters.

The initialization to zero ensures that `i` has a defined value before
entering the loop scope, satisfying static analysis requirements
while preserving the existing logic. The for loop immediately assigns
i to the first value from the range, so the initialization value is
never actually used in normal execution paths.

This change resolves the pyright reportPossiblyUnbound error without
altering the function's behavior or performance characteristics.

Signed-off-by: Wander Lairson Costa <redacted>
---
 tools/verification/rvgen/rvgen/ltl2k.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index fa9ea6d597095..94dc64af1716d 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py

@@ -45,6 +45,7 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
 
     abbrs = []
     for atom in atoms:
+        i = 0
         for i in range(len(atom), -1, -1):
             if sum(a.startswith(atom[:i]) for a in atoms) > 1:
                 break

-- 
2.52.0