z3 - PROOF_MODE オプションが使用されていない限り、未飽和応答

Question

リアルタイムタスクシステムで取得したスケジュールのロバスト性を証明するために Z3 を使用しています。このスクリプトhttp://www.cs.ru.nl/~georgeta/script.smt2を確認すると、unsat 応答が返されます。ただし、PROOF_MODE=1 オプションを使用すると、応答は sat になります。前者の場合、何が問題になる可能性がありますか?

Answer 1

あなたの例をダウンロードしました。指定されたロジックが正しくありません、コマンド：

（set-logic QF_AUFLIA）

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

そうは言っても、Z32.19で多くのバグを修正しました。新しいバージョン3.0はまもなくリリースされます。SMT-COMPに提出したプレリリース版はすでにご利用いただけます。