How to check constraint violation between 2 labels within never claim using SPIN?

Question

I'm experimenting with Promela and it's interpreter SPIN. I try to check that something does not happen between 2 points in the code, let's say between from and to the value of x does not leave a limit 3: x<=3:

int x=0;
active proctype F() {
  x = 10;
  x++;
from:
  x = 3;
  x = 300;
  x = 500;
to:
  x = 100;
  x++;
}

I open this site https://matthewbdwyer.github.io/psp/ of the professor Matthew Dwyer with LTL-patterns and follow links: The patterns -> Occurrence Patterns -> Absence -> LTL because it seems this is the right classification of my case and get here:

where I copy this formula:

Between Q and R	[]((Q & !R & <>R) -> (!P U R))

and pass it to the SPIN: spin -f "[]((f && !t && <>t) -> (!p U t))" >> p1.pml (converting it to convenient Promela syntax). And my code now looks:

#define p (x<=3)
#define f (F@from)
#define t (F@to)
int x=0;
active proctype F() {
  x = 10;
  x++;
from:
  x = 3;
  x = 300;
  x = 500;
to:
  x = 100;
  x++;
}
never  {    /* []((f && !t && <>t) -> (!p U t)) */
T0_init:
        do
        :: (((! ((f))) || ((t)))) -> goto accept_S141
        :: (! ((t))) -> goto accept_S47
        :: (! ((p))) -> goto T0_S165
        od;
accept_S47:
        do
        :: (! ((t))) -> goto T0_S47
        :: (! ((p)) && ! ((t))) -> goto T0_S95
        od;
accept_S165:
        do
        :: (! ((p)) && ! ((t))) -> goto T0_S95
        :: ((t)) -> goto T0_init
        :: (! ((p))) -> goto T0_S165
        od;
accept_S141:
        do
        :: (((! ((f))) || ((t)))) -> goto T0_init
        :: (! ((t))) -> goto T0_S47
        :: (! ((p))) -> goto T0_S165
        od;
T0_S47:
        do
        :: (! ((t))) -> goto accept_S47
        :: (! ((p)) && ! ((t))) -> goto T0_S95
        od;
T0_S95:
        do
        :: (! ((p)) && ! ((t))) -> goto T0_S95
        od;
T0_S165:
        do
        :: (! ((p)) && ! ((t))) -> goto T0_S95
        :: ((t)) -> goto accept_S141
        :: (! ((p))) -> goto T0_S165
        :: (! ((p)) && (t)) -> goto accept_S165
        od;
}

build: spin -a p1.pml, gcc -o p1 pan.c and run ./p1 -a and I see output:

warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)

(Spin Version 6.5.2 -- 30 May 2023)
    + Partial Order Reduction

Full statespace search for:
    never claim             + (never_0)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 28 byte, depth reached 10, errors: 0
       13 states, stored (25 visited)
       11 states, matched
       36 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001   equivalent memory usage for states (stored*(State-vector + overhead))
    0.286   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage


unreached in proctype F
    p1.pml:14, state 7, "x = (x+1)"
    p1.pml:15, state 8, "-end-"
    (2 of 8 states)
unreached in claim never_0
    p1.pml:56, state 58, "-end-"
    (1 of 58 states)

pan: elapsed time 0 seconds

It's strange because line 10 obviously violates never-claim. Then I change the line 9 from x = 3 to x = 4 and after run the simulation prints:

warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan:1: acceptance cycle (at depth 16)
pan: wrote p1.pml.trail

(Spin Version 6.5.2 -- 30 May 2023)
Warning: Search not completed
    + Partial Order Reduction

Full statespace search for:
    never claim             + (never_0)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 28 byte, depth reached 17, errors: 1
       14 states, stored (19 visited)
        4 states, matched
       23 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001   equivalent memory usage for states (stored*(State-vector + overhead))
    0.286   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage



pan: elapsed time 0 seconds

so I run the trail:

./spin -t -c p1.pml
proc 0 = F
starting claim 1
Never claim moves to line 19    [((!((F._p==from))||(F._p==to)))]
Never claim moves to line 36    [((!((F._p==from))||(F._p==to)))]
Never claim moves to line 21    [(!((x<=3)))]
Never claim moves to line 53    [(!((x<=3)))]
Never claim moves to line 52    [((F._p==to))]
Never claim moves to line 36    [((!((F._p==from))||(F._p==to)))]
Never claim moves to line 19    [((!((F._p==from))||(F._p==to)))]
      <<<<<START OF CYCLE>>>>>
Never claim moves to line 36    [((!((F._p==from))||(F._p==to)))]
Never claim moves to line 19    [((!((F._p==from))||(F._p==to)))]
spin: trail ends after 18 steps
-------------
final state:
-------------
#processes: 0
        x = 101
 18:    proc  - (never_0:1) p1.pml:35 (state 32)
1 processes created

so SPIN found the problem but after "to:" label which is very strange: 1) I changed 9th line to x = 4, 2) it should check before "to:" label, not after it. It looks as SPIN treats the snippet

x = 3;
x = 300;
x = 500;

as one state OR it checks only the first statement of this fragment ("from...to") but reports the problem in the next "state" (after "to:"). I checked states with ./p1 -D and get this diagram that looks correct to me (it's without never claim) - all assignments are different states. Then why does SPIN work in so strange way? Or where is the error in my reasoning?