Z3の.NETAPIを使用しています。次のように呼び出してソルバーをインスタンス化すると、次のようになります。
Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit));
一部のモデルでは、60秒（60000ミリ秒）のTimeLimitを指定します。
s.Check()
60秒後には戻りません。一部のモデルでは数秒後に戻りますが、私の場合は問題ありませんが、一部のモデルではまったく戻りません（3日後にプロセスをキャンセルしました）。
指定された制限時間後にZ3にチェックを停止させるにはどうすればよいですか？
TryForコンビネータは、「キャンセル」フラグを使用して実装されます。新しい戦術は非常に反応が良く、「キャンセル」フラグが設定されると非常に迅速に終了します。残念ながら、汎用戦術smtは汎用ソルバーのラッパーです。この汎用ソルバーはあまり応答性がありません。数量詞のインスタンス化、シンプレックスなど、いくつかの重要な場所で「失われる」可能性があります。この戦術は、および他の多くの戦術qfliaの上に構築されています。smt以来、あなたは数量詞のない問題を解決しようとしています。smt戦術はシンプレックスモジュール内のループにあると思います。戦術のシンプレックスモジュールは、smt任意精度の有理数を使用して実装されます。したがって、自明でない線形実数/整数問題の場合、非常に時間がかかる可能性があります。
この問題を回避するためにできることはあまりありません。実行時間の強力な保証が本当に必要な場合、私が見る唯一の解決策は、Z3を実行する別のプロセスを作成しk、問題の解決に数秒かかるたびにそれを強制終了することです。
そうは言っても、Z3の将来のバージョンには完全に新しい算術モジュールがあります。この新しいモジュール（新しい戦術と同様）は、キャンセルフラグが設定されるとすぐに終了します。