It's possible for a user to enter constraints that will always fail (e.g. post(state.edx) == 5 && post(state.rdx) == 6).
We should attempt to detect these cases by applying all pre-condition constraints and all post-condition constraints respectively to an arbitrary state and checking if it is SAT. If it's UNSAT, the user asserted something contradictory and we shouldn't bother running.