No split on KEVM JUMPI

Steps to reproduce:

cd evm-semantics
make tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k.prove

Expected behavior: should pass

Actual behavior: Execution gets stuck with the following content of k cell:

JUMPI 559 bool2Word ( 0 <Int maxUInt160 &Int #asWord ( #range ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01`" [ 128 := #buf ( 32 , SIGV0:Int ) ++ #buf ( 32 , SIGV1:Int ) ] [ 192 := #buf ( 32 , SIGR0:Int ) ++ #buf ( 32 , SIGR1:Int ) ] [ 256 := #buf ( 32 , SIGS0:Int ) ++ #buf ( 32 , SIGS1:Int ) ] [ 320 := b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ] [ 320 := #ecrec ( #buf ( 32 , HASH:Int ) , #buf ( 32 , SIGV0:Int ) , #buf ( 32 , SIGR0:Int ) , #buf ( 32 , SIGS0:Int ) ) [ 0 .. minInt ( 32 , #sizeByteArray ( #ecrec ( #buf ( 32 , HASH:Int ) , #buf ( 32 , SIGV0:Int ) , #buf ( 32 , SIGR0:Int ) , #buf ( 32 , SIGS0:Int ) ) ) ) ] ] , 320 , 32 ) ) )

It should split on JUMPI insteadm, based on these rules:

    rule <k> JUMPI _DEST I => . ... </k>
      requires I ==Int 0

    rule <k> JUMPI  DEST I => JUMP DEST ... </k>
      requires I =/=Int 0