(Binary Analysis) Don't call SMT solver if the answer is obvious

If the assertions are all known to be true then return SAT immediately.
If any assertion is known to be false then return UNSAT immediately.
Remove any known true assertions before calling the SMT solver.

This also works around a Yices problem where:

	(assert (mk-bv 1 0))
	(check)

fails.