title: Executing get-model or unsat-core depending on solver's decision
body: <p>I wonder, if there is a possibility in a SMT-LIB 2.0 script to access the last satisfiability decision of a solver (sat, unsat, ...). For example, the following code:</p>
  
  <pre><code>(set-option :produce-unsat-cores true)
  (set-option :produce-models true)
  (set-logic QF_UF)
  (declare-fun p () Bool)
  (declare-fun q () Bool)
  (declare-fun r () Bool)
  
  (assert (! (=&gt; p q) :named PQ))
  (assert (! (=&gt; q r) :named QR))
  (assert (! (not (=&gt; p r)) :named nPR))
  
  (check-sat)
  (get-model)
  (get-unsat-core)
  </code></pre>
  
  <p>ran in Z3 returns:</p>
  
  <pre><code>unsat
  (error "line 15 column 10: model is not available")
  (PQ QR nPR)
  </code></pre>
  
  <p>and ran in MathSAT returns:</p>
  
  <pre><code>unsat
  (error "model generation not enabled")
  </code></pre>
  
  <p>In MathSAT 5 it just breaks on (get-model) and doesn't even reach (get-unsat-core).
  Is there any way in SMT-LIB 2.0 language to get-model iff the decision was SAT and unsat-core iff the decision was UNSAT? Solution could for example look like this:</p>
  
  <pre><code>(check-sat)
  (ite (= (was-sat) true) (get-model) (get-unsat-core))
  </code></pre>
  
  <p>I searched SMT-LIB 2.0 language documentation, but I did not found any hint.</p>
  
  <p>EDIT:
  I also tried the code below, and unfortunately it did not work.</p>
  
  <pre><code>(ite (= (check-sat) "sat") (get-model) (get-unsat-core))
  </code></pre>