Verifier fails to detect infinite loops on conditional jumps

[Alan-Jowett]

All these tests should fail, but currently pass:

---
test-case: simple infinite loop, less than
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 0
    if r0 < 1 goto <start>
    exit

post: []

messages:
  - "1:2: Code is unreachable after 1:2"
# Message that should be generated by the verifier, but isn't:
#  - "Could not prove termination."
---
test-case: simple infinite loop, less than or equal
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 0
    if r0 <= 1 goto <start>
    exit

post: []

messages:
  - "1:2: Code is unreachable after 1:2"
# Message that should be generated by the verifier, but isn't:
#  - "Could not prove termination."

---
test-case: simple infinite loop, equal
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 0
    if r0 == 0 goto <start>
    exit

post: []

messages:
  - "1:2: Code is unreachable after 1:2"
# Message that should be generated by the verifier, but isn't:
#  - "Could not prove termination."

---
test-case: simple infinite loop, greater than
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 1
    if r0 > 0 goto <start>
    exit

post: []

messages:
  - "1:2: Code is unreachable after 1:2"
# Message that should be generated by the verifier, but isn't:
#  - "Could not prove termination."

---
test-case: simple infinite loop, greater than or equal
options: ["termination"]

pre: []

code:
  <start>: |
    r0 = 1
    if r0 >= 0 goto <start>
    exit

post: []

messages:
  - "1:2: Code is unreachable after 1:2"
# Message that should be generated by the verifier, but isn't:
#  - "Could not prove termination."