Pathological BPF program can force long veriifcation times

[Alan-Jowett]

Test case that causes the verifier to hang

test-case: Found by fuzzing
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 0
    r1 = 10
  <loop>: |
    w1 -= 1
    if r1 > 0 goto <loop>
    exit

post: []

[Alan-Jowett]

Not sure if the time is in fact bounded, but it takes > 10 minutes

[elazarg]

We know for a fact that the current implementation of the numeric domain can diverge, due to changes I've introduced, which broke widening in some cases. I don't know if that's the underlying cause here.

[Alan-Jowett]

This appears to be related to 32bit ALU ops. If I switch it to r1 -= 1 it converges.

[Alan-Jowett]

This is actually a test case generated by DiffSpec