z3 - Z3 の同じコードの異なる実行時間

Question

z3 の固定小数点を使用しましたが、固定小数点の実行時間が常に異なることがわかりました。同じ問題に遭遇しましたか？なぜこれが起こるのですか？

Answer 1

同じ状態から始まる同じコードの多様性が大きくなると、予想外に聞こえます。異なる状態から開始した場合 (つまり、ラウンド間で、テキスト API またはプログラム API を介して Z3 にさまざまな呼び出しを行った場合)。それ以外の場合、Z3 は非常に非決定論的な動作を示すべきではありません。非決定論的な動作はバグから発生する可能性があるため、それを実行しているシナリオをさらに正確に説明していただければ幸いです。