Check that assumptions are satisfiable

[atomb]

It would be convenient to check that specification preconditions are satisfiable, since unsatisfiable preconditions are almost certainly a mistake (unless being used to disallow a function from being called). It may make sense to do this by checking the satisfiability of the path condition right before starting symbolic execution, to ensure that we keep track of all conditions that have accumulated, whether implicit or explicit.

[langston-barrett]

This is done for Crucible/LLVM, but not elsewhere:

saw-script/src/SAWScript/Crucible/LLVM/Override.hs

Lines 500 to 504 in 90cd4da

	[ "The conjunction of these overrides' preconditions"
	, "was unsatisfiable, meaning your override can never"
	, "apply. You probably have unintentionally specified"
	, "mutually exclusive/inconsistent preconditions."
	]) PP.<$$>

[jldodds]

I'm still interested in this issue, although it could definitely introduce performance problems as well.

I'd also like a prove command that checks for trivial implication proofs. Does that belong in this issue or should it have its own?