Tag Theorem and LLVMSpec values that were proved by unsound means

[brianhuffman]

Whenever we produce a Theorem, LLVMSpec, or JVMSpec value as the result of a proof command, it should be specially marked as "unsafe" if any of the lemmas or proof tactics used to produce it were themselves "unsafe". In particular, anything proved using assume_unsat or llvm_unsafe_assume_spec should be marked as unsafe.

In addition to a single "unsafe" bit, we may also wish to record more detailed information about what the sources of the unsafeness were.

This information would be useful to display as part of a verification summary (see also #643).

[robdockins]

This is closely related to #1136