While testing with the switch.c code i've found out that the final state that we get after the replay is unsatisfiable and it is most likely that the constraint that is added in line 109 (to add constraint that the switch variable is equal with the recorded value) made the state unsatisfiable. I've try to look for the constraint given for that variable after the replay but i could figure out how to do that therefore i'm quite stuck at this point.
to replicate the bug you just need to record the switchi.c program (run with ./switchi) and replay. The state we get after the replay is unsatisfiable (state.solver.satisfiable() returns False)
While testing with the switch.c code i've found out that the final state that we get after the replay is unsatisfiable and it is most likely that the constraint that is added in line 109 (to add constraint that the switch variable is equal with the recorded value) made the state unsatisfiable. I've try to look for the constraint given for that variable after the replay but i could figure out how to do that therefore i'm quite stuck at this point.
to replicate the bug you just need to record the switchi.c program (run with ./switchi) and replay. The state we get after the replay is unsatisfiable (
state.solver.satisfiable()
returnsFalse
)