I already came up with an idea to solve the speed problem here. Put in an extra compiler flag that specifies how long the compiler can take to execute the SAT solver; once the time is up, no more SAT solving. Instead, you emit less optimized code that is known to be correct, but possibly slower than fully optimized code.