PROOF_MODEオプションが使用されていない場合は応答がありません

Question

私はリアルタイムタスクシステムで得られたスケジュールの堅牢性を証明するためにZ3を使用しています。このスクリプトをチェックすると、http://www.cs.ru.nl/~georgeta/script.smt2私は不満な応答を得ます。しかし、PROOF_MODE = 1オプションを使用すると、応答は飽和します。前者の場合、何が間違っている可能性がありますか？

Answer 1

私はあなたの例をダウンロードしました。

（セット・ロジックQF_AUFLIA）

このロジックは、スクリプトは配列のみ、未解釈の関数と整数の変数、および無数量が含まれますことを指定します。指定された論理は間違って、コマンドです。ただし、Real変数が含まれています。 このコマンドを削除すると、どちらの場合でも正しい答え（sat）が得られます。 Z3のプリプロセッサの中にはプルーフ生成をサポートしていないものがあるため、PROOF_MODE = 1を使用するときに異なる回答があります。プルーフ生成がオンになっていると無効になります。

つまり、私たちはZ3 2.19に多くのバグを修正しました。新しいバージョン3.0はすぐにリリースされる予定です。 SMT-COMPに提出したプレリリース版はすでに使用できます。