On Tue, Jan 20, 2026 at 01:30:35PM +0100, Gabriele Monaco wrote:

On Tue, 2026-01-20 at 08:37 -0300, Wander Lairson Costa wrote:

quoted

On Tue, Jan 20, 2026 at 09:59:11AM +0100, Gabriele Monaco wrote:

quoted

On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:

quoted

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.

So are we just pleasing the tool or is there a real implication of this?

Apparently code like

for i in range(len([]), -1, -1):
    pass
print(i)

works just fine since range() returns at least 0 (as you mentioned in the
commit
message) and i is not used before assignation in the loop, so I don't really
see
a problem.

Apparently pyright devs don't want ([1]) to implement a logic to sort out
the
/possibly/ unbound error here.

From what I understand, this code is already not pythonic, so rather than
silence the warning to please this tool I'd just refactor the code not to
use i
after the loop (or leave it as it is, since it works fine).

What do you think?

You're right, I could have done:

for atom in reversed(atoms): ...

I'm missing what you mean with this, the range is iterating over the string
representation of atom (in reverse) not the array of atoms.

Sorry, I misinterpreted you previous comment and picked the wrong piece
of code.

Yes, the basic goal was to make pyright happy.

You basically want i to be the length of the longest prefix common to at least
another atom.

You could assign i to some python trick doing the exact same thing the loop
does, like:

    i = next((i for i in range(len(atom), -1, -1)
        if sum(a.startswith(atom[:i]) for a in atoms) > 1))

next() is basically doing the break at the first occurrence from the generator,
just now your i doesn't live (only) inside the loop.

So now you save 2 lines and get any C developer scratch their head when they
look at the code, but hey, pyright is happy!

Or just leave the assignment.

If you do find the trick with next() readable or have any better idea, feel free
to try though.

Definitely the next() trick is not worth to make pyright happy.

Thanks,
Gabriele

quoted

I will modify it in v2.

quoted

Thanks,
Gabriele

[1] - https://github.com/microsoft/pyright/issues/844

quoted

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