It should be possible to use a SMT solver to automatically check for code for which the -O0 version has observably different behavior than the -O3 version for s

It should be possible to use a SMT solver to automatically check for code for which the -O0 version has observably different behavior than the -O3 version for some inputs to the program. Though I'm not sure current SMT solvers are up to the task. (Related: I was using Sugar for something a while back, only to find it was spitting out weird error messages. Turns out it encodes integers as <size of domain> boolean variables, which doesn't work particularly well for large domains - it was hitting a 4 (2?) GB limit on the size of the temporary SAT input file and choking)