[CN-Exec] Provide counterexample reproduction code

[ZippeyKeys12]

Given a memory state and a CN specification which is satisfied by that state, can we provide C code which would produce a similar state?

If so, you could print reproduction code of counterexample via the instrumentation. You'd have a stack where a new counterexample gets pushed after a precondition is successfully checked, and popped after a postcondition is successfully checked.

Note that a "similar" state might not actually reproduce a bug, since the program under test might only exhibit buggy behavior when a pointer has a specific property that isn't preserved by the reproduction code.

[ZippeyKeys12]

This also has a secondary benefit of making it easy to use our generators for suites of concrete test cases (run generator and get reproduction code).