XSTS initialization at declaration not working

[AdamZsofi]

We ( with @arminzavada ) are working on generating traces for XSTS generated by Semantifyr and found an example, where the state space was exploding, though it shouldn't:
inlined.xsts.txt

This should be a really simple model, where the only variable i is fairly constrained:

If you check the xsts, i is initialized in line 2:

var $$root$$system$$i$$value: integer = 0

but it's not initialized in init.
The other variables are either initialized in init or constrained at the beginning of trans. Also, I think Gamma always initialized everything in init, that's why this never came up.

I am not sure where the information is lost. What I see is that using explicit ARG building, I have i in the precision, but it's unknown in the first nodes and then successor computation explodes where i starts to matter - it never terminates. If I add $$root$$system$$Behaviour$$activeState := 0; in init, it works as intended.

@mondokm this is a bug, not a feature, right? If bug, can you please help finding the source of it and the fix?
Thanks a lot!

[mondokm]

What algorithm are you using? (mainly Domain, InitPrec, Maxenum are interesting)

Even if you are using EXPL domain, maxenum=1 could cause the algorithm to overapproximate i with top if it can have two different values after a transition