There's a very simple solver that completes that goal: one that reports that it cannot prove any code as correct. So there must be a secondary goal of "maximize the amount of accepted code", which is a significantly less trivial question.