The pull request https://github.com/fp-analysis/klee/pull/58 changed the constraints with error being updated when the comparison instructions were being executed. As a result, the path condition with error contains erroneous true and false conditions (example attached).
Correct this issue by adding a new field to the Cell object, to contain conditions with error so that the bindlocal call can updated it thereby allowing the constraints with error to be updated when the branch instructions is executed.
The pull request https://github.com/fp-analysis/klee/pull/58 changed the constraints with error being updated when the comparison instructions were being executed. As a result, the path condition with error contains erroneous true and false conditions (example attached).
Correct this issue by adding a new field to the Cell object, to contain conditions with error so that the bindlocal call can updated it thereby allowing the constraints with error to be updated when the branch instructions is executed.