[dorianh]

If I understand correctly, the authors feared that C-Reduce could introduce undefined behaviors:

> Unfortunately, if given the opportunity by a lax predicate, C-Reduce will write programs that have undefined behavior

I don't think this is true, in the introduction of [1]:

> Our reducers do this automatically and without introducing undefined behavior into the reduced test cases

[1] https://users.cs.utah.edu/~regehr/papers/pldi12-preprint.pdf