If I understand correctly, the authors feared that C-Reduce could introduce undefined behaviors: > Unfortunately, if given the opportunity by a lax predicate,

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 https://users.cs.utah.edu/~regehr/papers/pldi12-preprint.pdf