私はリアルタイムタスクシステムで得られたスケジュールの堅牢性を証明するためにZ3を使用しています。このスクリプトをチェックすると、http://www.cs.ru.nl/~georgeta/script.smt2私は不満な応答を得ます。しかし、PROOF_MODE = 1オプションを使用すると、応答は飽和します。前者の場合、何が間違っている可能性がありますか?PROOF_MODEオプションが使用されていない場合は応答がありません
2
A
答えて
2
私はあなたの例をダウンロードしました。
(セット・ロジックQF_AUFLIA)
このロジックは、スクリプトは配列のみ、未解釈の関数と整数の変数、および無数量が含まれますことを指定します。指定された論理は間違って、コマンドです。ただし、Real変数が含まれています。 このコマンドを削除すると、どちらの場合でも正しい答え(sat)が得られます。 Z3のプリプロセッサの中にはプルーフ生成をサポートしていないものがあるため、PROOF_MODE = 1を使用するときに異なる回答があります。プルーフ生成がオンになっていると無効になります。
つまり、私たちはZ3 2.19に多くのバグを修正しました。新しいバージョン3.0はすぐにリリースされる予定です。 SMT-COMPに提出したプレリリース版はすでに使用できます。
関連する問題
- 1. AJAXの応答が遅い場合は、リスト行が表示されません。
- 2. @propertyが使用されない場合があります
- 3. TouchJSONを使用している場合、「NSDictionary」が「+ dictionaryWithJSONString」に応答しない可能性があります。
- 4. crtmqm応答がありません
- 5. 応答がありませんサーバーソケットJava
- 6. オプションがチェックされている場合はaddClassを行いません
- 7. エクスプレスプロキシルートを使用した応答がありません
- 8. ません応答データカサンドラのJMeterを使用している場合
- 9. cell.backgroundColorのtableViewに設定した場合、応答がありません:cellForRowAtIndexPath
- 10. pythonw.exeが応答していません
- 11. httpストリーミング応答がサポートされていませんメッセージタイプ:class org.jboss.netty.handler.stream.ChunkedStream
- 12. http応答でデータが更新されていません
- 13. 何かが実行されている場合に終了オプションがありません
- 14. サーバからの応答が非常に遅い場合に応答が返されないasp.net
- 15. Authorize.Netサイレントポストが応答しない - 全くデータがありません
- 16. アプリがバックグラウンドモードの場合、リクエストは送信されません。オプション
- 17. JSON Web API .. PHPで消費されても応答がありません
- 18. ポストグラムでLIMITが使用されている場合はインデックスが使用されません
- 19. 応答が遅い場合はASIHTTPRequestがクラッシュします
- 20. using節が使用されている場合、DbConnectionを閉じる必要はありませんか?
- 21. IE用Rails 3.1アプリが壊れていて、jQueryイベントが応答しません。
- 22. ICEpush 3.0.1は、JBoss 7.1.1では応答がありません
- 23. JavaScriptファイルがない場合、ページはロードされません
- 24. 意図が投稿されない場合があります
- 25. Android USBが認識されない場合があります
- 26. データの場合はForm_validationが実行されていません
- 27. snmpset/getが返すタイムアウト:ipv6の応答がありません
- 28. WPFアプリが応答しない場合は、自動再起動
- 29. angular $ httpBackend.when mock - 遅延応答がグローバルではありません
- 30. モンゴースの作成方法には応答がありません
ありがとうございました!確かに、間違ったロジックが使用されました... set-logicコマンドがオプションであることを知っておくとよいでしょう。 –