z3 - 遷移システムのカウンター ループ - Z3

Question

Z3 の PDR エンジンを使用して、遷移系の不変式を証明します。遷移システムに、特定の状態に到達するために通過する必要があるカウンター ループが含まれている場合、パフォーマンスは低下します。

次のソース コードでは、 Z3 Fixedpoint Homepageの遷移システム Python クラスで実装された 3 つの状態と 3 つの遷移を含む遷移システムの例を示します。最後の行には、状態 L0 から開始して状態 L2 に到達するクエリがあります。したがって、遷移 t2 は y 回通過する必要があります。

y==10 を初期化すると、答えは高速に計算されます。ただし、初期化 y==1000 ではパフォーマンスが低下します。

L0 = L.L0 
L1 = L.L1
L2 = L.L2
y=Int('y')
i = Int('i')
state  = Const('state', L)

t1 = { "guard" : state == L0,
   "effect" : [ L1, i ] }
t2 = { "guard" : And(state == L1),
   "effect" : [ L1, i+1 ] }
t3 = { "guard" : And(state == L1,i>y),
   "effect" : [ L2, i]}

ptr = TransitionSystem( And(state == L0, i == 0, y==10),[t1, t2, t3],[state, i])
ptr.query(state==L2)

L0 から L2 へのパスを別の方法で計算し、Z3 のパフォーマンスを向上させる可能性はありますか?