Inconsistent report of verification results

[Danil Sokolov]

Verification result are reported as "violating" or "satisfying" the checked property. "Violating" means a trace exists that satisfies the Reach predicate. "Satisfying" means no trace satisfies the Reach predicate. This is confusing.

A solution is to add satisfiableMessage and unsatisfyableMessage to the MpsatSettings, so the report for each verification property can be fine-tuned.