Supose we do path exploration on this program

int main()
{
  int x;
  if(x)
    assert(0);
  else
    assert(0);
}

by running

cbmc  --paths lifo /tmp/foo.c

the output indicates that both paths were explored. However, in each case, the assertion on the other path is printed as being successful, even though it clearly fails, because that path was not the one currently under consideration:

...
** Results:
[main.assertion.1] assertion 0: SUCCESS
[main.assertion.2] assertion 0: FAILURE

** 1 of 2 failed (2 iterations)
VERIFICATION FAILED
___________________________
Starting new path (1 to go)
...
** Results:
[main.assertion.1] assertion 0: FAILURE
[main.assertion.2] assertion 0: SUCCESS

** 1 of 2 failed (2 iterations)
VERIFICATION FAILED

we should not print a spurious SUCCESS result for assertions that lie on a path that we're not currently exploring.