z3 - ソルバーの決定に応じて get-model または unsat-core を実行する

Question

SMT-LIB 2.0 スクリプトで、ソルバーの最後の充足可能性の決定 (sat、unsat、...) にアクセスする可能性があるかどうか疑問に思います。たとえば、次のコード:

(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 (! (=> p q) :named PQ))
(assert (! (=> q r) :named QR))
(assert (! (not (=> p r)) :named nPR))

(check-sat)
(get-model)
(get-unsat-core)

Z3 で実行:

unsat
(error "line 15 column 10: model is not available")
(PQ QR nPR)

MathSAT で実行すると、次のように返されます。

unsat
(error "model generation not enabled")

MathSAT 5 では、ブレークオン (get-model) するだけで、到達すらしません (get-unsat-core)。SMT-LIB 2.0 言語で、決定が SAT の場合に get-model を実行し、決定が UNSAT の場合に unsat-core を実行する方法はありますか? ソリューションは、たとえば次のようになります。

(check-sat)
(ite (= (was-sat) true) (get-model) (get-unsat-core))

SMT-LIB 2.0 言語のドキュメントを検索しましたが、ヒントは見つかりませんでした。

編集:以下のコードも試しましたが、残念ながら機能しませんでした。

(ite (= (check-sat) "sat") (get-model) (get-unsat-core))