unknown Initial ITS Start location: l2 Program variables: i1^0 i2^0 i3^0 i4^0 i5^0 i6^0 i7^0 i8^0 n17^0 n21^0 n25^0 n29^0 n33^0 n37^0 n41^0 n45^0 ret18^0 ret22^0 ret26^0 ret30^0 ret34^0 ret38^0 ret42^0 ret46^0 ret_fn120^0 ret_fn124^0 ret_fn128^0 ret_fn132^0 ret_fn136^0 ret_fn140^0 ret_fn144^0 ret_fn148^0 tmp19^0 tmp23^0 tmp27^0 tmp31^0 tmp35^0 tmp39^0 tmp43^0 tmp47^0 tmp^0 tmp___0^0 tmp___1^0 tmp___2^0 tmp___3^0 tmp___4^0 tmp___5^0 tmp___6^0 0: l0 -> l1 : i1^0'=i1^post1, i2^0'=i2^post1, i3^0'=i3^post1, i4^0'=i4^post1, i5^0'=i5^post1, i6^0'=i6^post1, i7^0'=i7^post1, i8^0'=i8^post1, n17^0'=n17^post1, n21^0'=n21^post1, n25^0'=n25^post1, n29^0'=n29^post1, n33^0'=n33^post1, n37^0'=n37^post1, n41^0'=n41^post1, n45^0'=n45^post1, ret18^0'=ret18^post1, ret22^0'=ret22^post1, ret26^0'=ret26^post1, ret30^0'=ret30^post1, ret34^0'=ret34^post1, ret38^0'=ret38^post1, ret42^0'=ret42^post1, ret46^0'=ret46^post1, ret_fn120^0'=ret_fn120^post1, ret_fn124^0'=ret_fn124^post1, ret_fn128^0'=ret_fn128^post1, ret_fn132^0'=ret_fn132^post1, ret_fn136^0'=ret_fn136^post1, ret_fn140^0'=ret_fn140^post1, ret_fn144^0'=ret_fn144^post1, ret_fn148^0'=ret_fn148^post1, tmp19^0'=tmp19^post1, tmp23^0'=tmp23^post1, tmp27^0'=tmp27^post1, tmp31^0'=tmp31^post1, tmp35^0'=tmp35^post1, tmp39^0'=tmp39^post1, tmp43^0'=tmp43^post1, tmp47^0'=tmp47^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, tmp___2^0'=tmp___2^post1, tmp___3^0'=tmp___3^post1, tmp___4^0'=tmp___4^post1, tmp___5^0'=tmp___5^post1, tmp___6^0'=tmp___6^post1, (0 == 0 /\ -2+n29^post1 == 0 /\ -ret_fn148^post1+tmp___6^post1 == 0 /\ -tmp___6^post1+i8^post1 == 0 /\ ret_fn128^post1-ret26^post1 == 0 /\ ret18^post1-tmp19^post1 == 0 /\ -ret22^post1+ret_fn124^post1 == 0 /\ -2+n33^post1 == 0 /\ -tmp___0^post1+i2^post1 == 0 /\ -2+n21^post1 == 0 /\ -2+n45^post1 == 0 /\ ret38^post1-tmp39^post1 == 0 /\ -tmp___4^post1+i6^post1 == 0 /\ -tmp___1^post1+i3^post1 == 0 /\ ret_fn136^post1-ret34^post1 == 0 /\ tmp___0^post1-ret_fn124^post1 == 0 /\ -ret30^post1+ret_fn132^post1 == 0 /\ ret46^post1-tmp47^post1 == 0 /\ -tmp___3^post1+i5^post1 == 0 /\ ret_fn148^post1-ret46^post1 == 0 /\ -tmp27^post1+ret26^post1 == 0 /\ -ret18^post1+ret_fn120^post1 == 0 /\ -2+n37^post1 == 0 /\ -ret_fn120^post1+tmp^post1 == 0 /\ -ret_fn136^post1+tmp___3^post1 == 0 /\ ret30^post1-tmp31^post1 == 0 /\ -2+n25^post1 == 0 /\ -ret_fn144^post1+tmp___5^post1 == 0 /\ -ret_fn132^post1+tmp___2^post1 == 0 /\ -tmp___5^post1+i7^post1 == 0 /\ -ret42^post1+ret_fn144^post1 == 0 /\ ret34^post1-tmp35^post1 == 0 /\ -ret_fn140^post1+tmp___4^post1 == 0 /\ ret22^post1-tmp23^post1 == 0 /\ i4^post1-tmp___2^post1 == 0 /\ -ret_fn128^post1+tmp___1^post1 == 0 /\ -2+n17^post1 == 0 /\ ret42^post1-tmp43^post1 == 0 /\ -2+n41^post1 == 0 /\ i1^post1-tmp^post1 == 0 /\ ret_fn140^post1-ret38^post1 == 0), cost: 1 1: l2 -> l0 : i1^0'=i1^post2, i2^0'=i2^post2, i3^0'=i3^post2, i4^0'=i4^post2, i5^0'=i5^post2, i6^0'=i6^post2, i7^0'=i7^post2, i8^0'=i8^post2, n17^0'=n17^post2, n21^0'=n21^post2, n25^0'=n25^post2, n29^0'=n29^post2, n33^0'=n33^post2, n37^0'=n37^post2, n41^0'=n41^post2, n45^0'=n45^post2, ret18^0'=ret18^post2, ret22^0'=ret22^post2, ret26^0'=ret26^post2, ret30^0'=ret30^post2, ret34^0'=ret34^post2, ret38^0'=ret38^post2, ret42^0'=ret42^post2, ret46^0'=ret46^post2, ret_fn120^0'=ret_fn120^post2, ret_fn124^0'=ret_fn124^post2, ret_fn128^0'=ret_fn128^post2, ret_fn132^0'=ret_fn132^post2, ret_fn136^0'=ret_fn136^post2, ret_fn140^0'=ret_fn140^post2, ret_fn144^0'=ret_fn144^post2, ret_fn148^0'=ret_fn148^post2, tmp19^0'=tmp19^post2, tmp23^0'=tmp23^post2, tmp27^0'=tmp27^post2, tmp31^0'=tmp31^post2, tmp35^0'=tmp35^post2, tmp39^0'=tmp39^post2, tmp43^0'=tmp43^post2, tmp47^0'=tmp47^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, tmp___2^0'=tmp___2^post2, tmp___3^0'=tmp___3^post2, tmp___4^0'=tmp___4^post2, tmp___5^0'=tmp___5^post2, tmp___6^0'=tmp___6^post2, (tmp47^0-tmp47^post2 == 0 /\ -n25^post2+n25^0 == 0 /\ -n45^post2+n45^0 == 0 /\ n41^0-n41^post2 == 0 /\ ret38^0-ret38^post2 == 0 /\ -ret_fn124^post2+ret_fn124^0 == 0 /\ ret_fn132^0-ret_fn132^post2 == 0 /\ tmp23^0-tmp23^post2 == 0 /\ -i3^post2+i3^0 == 0 /\ -i8^post2+i8^0 == 0 /\ -ret_fn128^post2+ret_fn128^0 == 0 /\ -n37^post2+n37^0 == 0 /\ tmp39^0-tmp39^post2 == 0 /\ -i5^post2+i5^0 == 0 /\ -ret_fn148^post2+ret_fn148^0 == 0 /\ -tmp43^post2+tmp43^0 == 0 /\ -tmp___5^post2+tmp___5^0 == 0 /\ -i6^post2+i6^0 == 0 /\ -tmp___4^post2+tmp___4^0 == 0 /\ -ret30^post2+ret30^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ ret_fn120^0-ret_fn120^post2 == 0 /\ -tmp___6^post2+tmp___6^0 == 0 /\ ret22^0-ret22^post2 == 0 /\ tmp___2^0-tmp___2^post2 == 0 /\ -i7^post2+i7^0 == 0 /\ -i4^post2+i4^0 == 0 /\ ret_fn140^0-ret_fn140^post2 == 0 /\ -ret_fn136^post2+ret_fn136^0 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ ret46^0-ret46^post2 == 0 /\ n29^0-n29^post2 == 0 /\ -ret18^post2+ret18^0 == 0 /\ ret_fn144^0-ret_fn144^post2 == 0 /\ ret26^0-ret26^post2 == 0 /\ -tmp19^post2+tmp19^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ -tmp___3^post2+tmp___3^0 == 0 /\ -n33^post2+n33^0 == 0 /\ n17^0-n17^post2 == 0 /\ -i2^post2+i2^0 == 0 /\ -tmp31^post2+tmp31^0 == 0 /\ tmp27^0-tmp27^post2 == 0 /\ -n21^post2+n21^0 == 0 /\ tmp35^0-tmp35^post2 == 0 /\ -i1^post2+i1^0 == 0 /\ -ret42^post2+ret42^0 == 0 /\ ret34^0-ret34^post2 == 0), cost: 1 Chained Linear Paths Start location: l2 Program variables: i1^0 i2^0 i3^0 i4^0 i5^0 i6^0 i7^0 i8^0 n17^0 n21^0 n25^0 n29^0 n33^0 n37^0 n41^0 n45^0 ret18^0 ret22^0 ret26^0 ret30^0 ret34^0 ret38^0 ret42^0 ret46^0 ret_fn120^0 ret_fn124^0 ret_fn128^0 ret_fn132^0 ret_fn136^0 ret_fn140^0 ret_fn144^0 ret_fn148^0 tmp19^0 tmp23^0 tmp27^0 tmp31^0 tmp35^0 tmp39^0 tmp43^0 tmp47^0 tmp^0 tmp___0^0 tmp___1^0 tmp___2^0 tmp___3^0 tmp___4^0 tmp___5^0 tmp___6^0 2: l2 -> l1 : i1^0'=i1^post1, i2^0'=i2^post1, i3^0'=i3^post1, i4^0'=i4^post1, i5^0'=i5^post1, i6^0'=i6^post1, i7^0'=i7^post1, i8^0'=i8^post1, n17^0'=n17^post1, n21^0'=n21^post1, n25^0'=n25^post1, n29^0'=n29^post1, n33^0'=n33^post1, n37^0'=n37^post1, n41^0'=n41^post1, n45^0'=n45^post1, ret18^0'=ret18^post1, ret22^0'=ret22^post1, ret26^0'=ret26^post1, ret30^0'=ret30^post1, ret34^0'=ret34^post1, ret38^0'=ret38^post1, ret42^0'=ret42^post1, ret46^0'=ret46^post1, ret_fn120^0'=ret_fn120^post1, ret_fn124^0'=ret_fn124^post1, ret_fn128^0'=ret_fn128^post1, ret_fn132^0'=ret_fn132^post1, ret_fn136^0'=ret_fn136^post1, ret_fn140^0'=ret_fn140^post1, ret_fn144^0'=ret_fn144^post1, ret_fn148^0'=ret_fn148^post1, tmp19^0'=tmp19^post1, tmp23^0'=tmp23^post1, tmp27^0'=tmp27^post1, tmp31^0'=tmp31^post1, tmp35^0'=tmp35^post1, tmp39^0'=tmp39^post1, tmp43^0'=tmp43^post1, tmp47^0'=tmp47^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, tmp___2^0'=tmp___2^post1, tmp___3^0'=tmp___3^post1, tmp___4^0'=tmp___4^post1, tmp___5^0'=tmp___5^post1, tmp___6^0'=tmp___6^post1, (0 == 0 /\ tmp47^0-tmp47^post2 == 0 /\ -2+n29^post1 == 0 /\ -n25^post2+n25^0 == 0 /\ -ret_fn148^post1+tmp___6^post1 == 0 /\ -n45^post2+n45^0 == 0 /\ -tmp___6^post1+i8^post1 == 0 /\ n41^0-n41^post2 == 0 /\ ret38^0-ret38^post2 == 0 /\ ret_fn128^post1-ret26^post1 == 0 /\ -ret_fn124^post2+ret_fn124^0 == 0 /\ ret_fn132^0-ret_fn132^post2 == 0 /\ ret18^post1-tmp19^post1 == 0 /\ -ret22^post1+ret_fn124^post1 == 0 /\ -2+n33^post1 == 0 /\ tmp23^0-tmp23^post2 == 0 /\ -i3^post2+i3^0 == 0 /\ -i8^post2+i8^0 == 0 /\ -tmp___0^post1+i2^post1 == 0 /\ -ret_fn128^post2+ret_fn128^0 == 0 /\ -2+n21^post1 == 0 /\ -n37^post2+n37^0 == 0 /\ tmp39^0-tmp39^post2 == 0 /\ -i5^post2+i5^0 == 0 /\ -2+n45^post1 == 0 /\ -ret_fn148^post2+ret_fn148^0 == 0 /\ ret38^post1-tmp39^post1 == 0 /\ -tmp___4^post1+i6^post1 == 0 /\ -tmp43^post2+tmp43^0 == 0 /\ -tmp___1^post1+i3^post1 == 0 /\ ret_fn136^post1-ret34^post1 == 0 /\ tmp___0^post1-ret_fn124^post1 == 0 /\ -tmp___5^post2+tmp___5^0 == 0 /\ -i6^post2+i6^0 == 0 /\ -ret30^post1+ret_fn132^post1 == 0 /\ -tmp___4^post2+tmp___4^0 == 0 /\ -ret30^post2+ret30^0 == 0 /\ ret46^post1-tmp47^post1 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___3^post1+i5^post1 == 0 /\ ret_fn148^post1-ret46^post1 == 0 /\ -tmp27^post1+ret26^post1 == 0 /\ ret_fn120^0-ret_fn120^post2 == 0 /\ -tmp___6^post2+tmp___6^0 == 0 /\ ret22^0-ret22^post2 == 0 /\ tmp___2^0-tmp___2^post2 == 0 /\ -ret18^post1+ret_fn120^post1 == 0 /\ -2+n37^post1 == 0 /\ -i7^post2+i7^0 == 0 /\ -ret_fn120^post1+tmp^post1 == 0 /\ -i4^post2+i4^0 == 0 /\ ret_fn140^0-ret_fn140^post2 == 0 /\ -ret_fn136^post1+tmp___3^post1 == 0 /\ -ret_fn136^post2+ret_fn136^0 == 0 /\ ret30^post1-tmp31^post1 == 0 /\ -2+n25^post1 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ -ret_fn144^post1+tmp___5^post1 == 0 /\ ret46^0-ret46^post2 == 0 /\ n29^0-n29^post2 == 0 /\ -ret18^post2+ret18^0 == 0 /\ -ret_fn132^post1+tmp___2^post1 == 0 /\ ret_fn144^0-ret_fn144^post2 == 0 /\ -tmp___5^post1+i7^post1 == 0 /\ ret26^0-ret26^post2 == 0 /\ -ret42^post1+ret_fn144^post1 == 0 /\ -tmp19^post2+tmp19^0 == 0 /\ ret34^post1-tmp35^post1 == 0 /\ -ret_fn140^post1+tmp___4^post1 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ ret22^post1-tmp23^post1 == 0 /\ -tmp___3^post2+tmp___3^0 == 0 /\ -n33^post2+n33^0 == 0 /\ i4^post1-tmp___2^post1 == 0 /\ n17^0-n17^post2 == 0 /\ -i2^post2+i2^0 == 0 /\ -tmp31^post2+tmp31^0 == 0 /\ tmp27^0-tmp27^post2 == 0 /\ -ret_fn128^post1+tmp___1^post1 == 0 /\ -2+n17^post1 == 0 /\ -n21^post2+n21^0 == 0 /\ ret42^post1-tmp43^post1 == 0 /\ tmp35^0-tmp35^post2 == 0 /\ -i1^post2+i1^0 == 0 /\ -2+n41^post1 == 0 /\ i1^post1-tmp^post1 == 0 /\ -ret42^post2+ret42^0 == 0 /\ ret34^0-ret34^post2 == 0 /\ ret_fn140^post1-ret38^post1 == 0), cost: 1 Eliminating location l0 by chaining: Applied chaining First rule: l2 -> l0 : i1^0'=i1^post2, i2^0'=i2^post2, i3^0'=i3^post2, i4^0'=i4^post2, i5^0'=i5^post2, i6^0'=i6^post2, i7^0'=i7^post2, i8^0'=i8^post2, n17^0'=n17^post2, n21^0'=n21^post2, n25^0'=n25^post2, n29^0'=n29^post2, n33^0'=n33^post2, n37^0'=n37^post2, n41^0'=n41^post2, n45^0'=n45^post2, ret18^0'=ret18^post2, ret22^0'=ret22^post2, ret26^0'=ret26^post2, ret30^0'=ret30^post2, ret34^0'=ret34^post2, ret38^0'=ret38^post2, ret42^0'=ret42^post2, ret46^0'=ret46^post2, ret_fn120^0'=ret_fn120^post2, ret_fn124^0'=ret_fn124^post2, ret_fn128^0'=ret_fn128^post2, ret_fn132^0'=ret_fn132^post2, ret_fn136^0'=ret_fn136^post2, ret_fn140^0'=ret_fn140^post2, ret_fn144^0'=ret_fn144^post2, ret_fn148^0'=ret_fn148^post2, tmp19^0'=tmp19^post2, tmp23^0'=tmp23^post2, tmp27^0'=tmp27^post2, tmp31^0'=tmp31^post2, tmp35^0'=tmp35^post2, tmp39^0'=tmp39^post2, tmp43^0'=tmp43^post2, tmp47^0'=tmp47^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, tmp___2^0'=tmp___2^post2, tmp___3^0'=tmp___3^post2, tmp___4^0'=tmp___4^post2, tmp___5^0'=tmp___5^post2, tmp___6^0'=tmp___6^post2, (tmp47^0-tmp47^post2 == 0 /\ -n25^post2+n25^0 == 0 /\ -n45^post2+n45^0 == 0 /\ n41^0-n41^post2 == 0 /\ ret38^0-ret38^post2 == 0 /\ -ret_fn124^post2+ret_fn124^0 == 0 /\ ret_fn132^0-ret_fn132^post2 == 0 /\ tmp23^0-tmp23^post2 == 0 /\ -i3^post2+i3^0 == 0 /\ -i8^post2+i8^0 == 0 /\ -ret_fn128^post2+ret_fn128^0 == 0 /\ -n37^post2+n37^0 == 0 /\ tmp39^0-tmp39^post2 == 0 /\ -i5^post2+i5^0 == 0 /\ -ret_fn148^post2+ret_fn148^0 == 0 /\ -tmp43^post2+tmp43^0 == 0 /\ -tmp___5^post2+tmp___5^0 == 0 /\ -i6^post2+i6^0 == 0 /\ -tmp___4^post2+tmp___4^0 == 0 /\ -ret30^post2+ret30^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ ret_fn120^0-ret_fn120^post2 == 0 /\ -tmp___6^post2+tmp___6^0 == 0 /\ ret22^0-ret22^post2 == 0 /\ tmp___2^0-tmp___2^post2 == 0 /\ -i7^post2+i7^0 == 0 /\ -i4^post2+i4^0 == 0 /\ ret_fn140^0-ret_fn140^post2 == 0 /\ -ret_fn136^post2+ret_fn136^0 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ ret46^0-ret46^post2 == 0 /\ n29^0-n29^post2 == 0 /\ -ret18^post2+ret18^0 == 0 /\ ret_fn144^0-ret_fn144^post2 == 0 /\ ret26^0-ret26^post2 == 0 /\ -tmp19^post2+tmp19^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ -tmp___3^post2+tmp___3^0 == 0 /\ -n33^post2+n33^0 == 0 /\ n17^0-n17^post2 == 0 /\ -i2^post2+i2^0 == 0 /\ -tmp31^post2+tmp31^0 == 0 /\ tmp27^0-tmp27^post2 == 0 /\ -n21^post2+n21^0 == 0 /\ tmp35^0-tmp35^post2 == 0 /\ -i1^post2+i1^0 == 0 /\ -ret42^post2+ret42^0 == 0 /\ ret34^0-ret34^post2 == 0), cost: 1 Second rule: l0 -> l1 : i1^0'=i1^post1, i2^0'=i2^post1, i3^0'=i3^post1, i4^0'=i4^post1, i5^0'=i5^post1, i6^0'=i6^post1, i7^0'=i7^post1, i8^0'=i8^post1, n17^0'=n17^post1, n21^0'=n21^post1, n25^0'=n25^post1, n29^0'=n29^post1, n33^0'=n33^post1, n37^0'=n37^post1, n41^0'=n41^post1, n45^0'=n45^post1, ret18^0'=ret18^post1, ret22^0'=ret22^post1, ret26^0'=ret26^post1, ret30^0'=ret30^post1, ret34^0'=ret34^post1, ret38^0'=ret38^post1, ret42^0'=ret42^post1, ret46^0'=ret46^post1, ret_fn120^0'=ret_fn120^post1, ret_fn124^0'=ret_fn124^post1, ret_fn128^0'=ret_fn128^post1, ret_fn132^0'=ret_fn132^post1, ret_fn136^0'=ret_fn136^post1, ret_fn140^0'=ret_fn140^post1, ret_fn144^0'=ret_fn144^post1, ret_fn148^0'=ret_fn148^post1, tmp19^0'=tmp19^post1, tmp23^0'=tmp23^post1, tmp27^0'=tmp27^post1, tmp31^0'=tmp31^post1, tmp35^0'=tmp35^post1, tmp39^0'=tmp39^post1, tmp43^0'=tmp43^post1, tmp47^0'=tmp47^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, tmp___2^0'=tmp___2^post1, tmp___3^0'=tmp___3^post1, tmp___4^0'=tmp___4^post1, tmp___5^0'=tmp___5^post1, tmp___6^0'=tmp___6^post1, (0 == 0 /\ -2+n29^post1 == 0 /\ -ret_fn148^post1+tmp___6^post1 == 0 /\ -tmp___6^post1+i8^post1 == 0 /\ ret_fn128^post1-ret26^post1 == 0 /\ ret18^post1-tmp19^post1 == 0 /\ -ret22^post1+ret_fn124^post1 == 0 /\ -2+n33^post1 == 0 /\ -tmp___0^post1+i2^post1 == 0 /\ -2+n21^post1 == 0 /\ -2+n45^post1 == 0 /\ ret38^post1-tmp39^post1 == 0 /\ -tmp___4^post1+i6^post1 == 0 /\ -tmp___1^post1+i3^post1 == 0 /\ ret_fn136^post1-ret34^post1 == 0 /\ tmp___0^post1-ret_fn124^post1 == 0 /\ -ret30^post1+ret_fn132^post1 == 0 /\ ret46^post1-tmp47^post1 == 0 /\ -tmp___3^post1+i5^post1 == 0 /\ ret_fn148^post1-ret46^post1 == 0 /\ -tmp27^post1+ret26^post1 == 0 /\ -ret18^post1+ret_fn120^post1 == 0 /\ -2+n37^post1 == 0 /\ -ret_fn120^post1+tmp^post1 == 0 /\ -ret_fn136^post1+tmp___3^post1 == 0 /\ ret30^post1-tmp31^post1 == 0 /\ -2+n25^post1 == 0 /\ -ret_fn144^post1+tmp___5^post1 == 0 /\ -ret_fn132^post1+tmp___2^post1 == 0 /\ -tmp___5^post1+i7^post1 == 0 /\ -ret42^post1+ret_fn144^post1 == 0 /\ ret34^post1-tmp35^post1 == 0 /\ -ret_fn140^post1+tmp___4^post1 == 0 /\ ret22^post1-tmp23^post1 == 0 /\ i4^post1-tmp___2^post1 == 0 /\ -ret_fn128^post1+tmp___1^post1 == 0 /\ -2+n17^post1 == 0 /\ ret42^post1-tmp43^post1 == 0 /\ -2+n41^post1 == 0 /\ i1^post1-tmp^post1 == 0 /\ ret_fn140^post1-ret38^post1 == 0), cost: 1 New rule: l2 -> l1 : i1^0'=i1^post1, i2^0'=i2^post1, i3^0'=i3^post1, i4^0'=i4^post1, i5^0'=i5^post1, i6^0'=i6^post1, i7^0'=i7^post1, i8^0'=i8^post1, n17^0'=n17^post1, n21^0'=n21^post1, n25^0'=n25^post1, n29^0'=n29^post1, n33^0'=n33^post1, n37^0'=n37^post1, n41^0'=n41^post1, n45^0'=n45^post1, ret18^0'=ret18^post1, ret22^0'=ret22^post1, ret26^0'=ret26^post1, ret30^0'=ret30^post1, ret34^0'=ret34^post1, ret38^0'=ret38^post1, ret42^0'=ret42^post1, ret46^0'=ret46^post1, ret_fn120^0'=ret_fn120^post1, ret_fn124^0'=ret_fn124^post1, ret_fn128^0'=ret_fn128^post1, ret_fn132^0'=ret_fn132^post1, ret_fn136^0'=ret_fn136^post1, ret_fn140^0'=ret_fn140^post1, ret_fn144^0'=ret_fn144^post1, ret_fn148^0'=ret_fn148^post1, tmp19^0'=tmp19^post1, tmp23^0'=tmp23^post1, tmp27^0'=tmp27^post1, tmp31^0'=tmp31^post1, tmp35^0'=tmp35^post1, tmp39^0'=tmp39^post1, tmp43^0'=tmp43^post1, tmp47^0'=tmp47^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, tmp___2^0'=tmp___2^post1, tmp___3^0'=tmp___3^post1, tmp___4^0'=tmp___4^post1, tmp___5^0'=tmp___5^post1, tmp___6^0'=tmp___6^post1, (0 == 0 /\ tmp47^0-tmp47^post2 == 0 /\ -2+n29^post1 == 0 /\ -n25^post2+n25^0 == 0 /\ -ret_fn148^post1+tmp___6^post1 == 0 /\ -n45^post2+n45^0 == 0 /\ -tmp___6^post1+i8^post1 == 0 /\ n41^0-n41^post2 == 0 /\ ret38^0-ret38^post2 == 0 /\ ret_fn128^post1-ret26^post1 == 0 /\ -ret_fn124^post2+ret_fn124^0 == 0 /\ ret_fn132^0-ret_fn132^post2 == 0 /\ ret18^post1-tmp19^post1 == 0 /\ -ret22^post1+ret_fn124^post1 == 0 /\ -2+n33^post1 == 0 /\ tmp23^0-tmp23^post2 == 0 /\ -i3^post2+i3^0 == 0 /\ -i8^post2+i8^0 == 0 /\ -tmp___0^post1+i2^post1 == 0 /\ -ret_fn128^post2+ret_fn128^0 == 0 /\ -2+n21^post1 == 0 /\ -n37^post2+n37^0 == 0 /\ tmp39^0-tmp39^post2 == 0 /\ -i5^post2+i5^0 == 0 /\ -2+n45^post1 == 0 /\ -ret_fn148^post2+ret_fn148^0 == 0 /\ ret38^post1-tmp39^post1 == 0 /\ -tmp___4^post1+i6^post1 == 0 /\ -tmp43^post2+tmp43^0 == 0 /\ -tmp___1^post1+i3^post1 == 0 /\ ret_fn136^post1-ret34^post1 == 0 /\ tmp___0^post1-ret_fn124^post1 == 0 /\ -tmp___5^post2+tmp___5^0 == 0 /\ -i6^post2+i6^0 == 0 /\ -ret30^post1+ret_fn132^post1 == 0 /\ -tmp___4^post2+tmp___4^0 == 0 /\ -ret30^post2+ret30^0 == 0 /\ ret46^post1-tmp47^post1 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___3^post1+i5^post1 == 0 /\ ret_fn148^post1-ret46^post1 == 0 /\ -tmp27^post1+ret26^post1 == 0 /\ ret_fn120^0-ret_fn120^post2 == 0 /\ -tmp___6^post2+tmp___6^0 == 0 /\ ret22^0-ret22^post2 == 0 /\ tmp___2^0-tmp___2^post2 == 0 /\ -ret18^post1+ret_fn120^post1 == 0 /\ -2+n37^post1 == 0 /\ -i7^post2+i7^0 == 0 /\ -ret_fn120^post1+tmp^post1 == 0 /\ -i4^post2+i4^0 == 0 /\ ret_fn140^0-ret_fn140^post2 == 0 /\ -ret_fn136^post1+tmp___3^post1 == 0 /\ -ret_fn136^post2+ret_fn136^0 == 0 /\ ret30^post1-tmp31^post1 == 0 /\ -2+n25^post1 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ -ret_fn144^post1+tmp___5^post1 == 0 /\ ret46^0-ret46^post2 == 0 /\ n29^0-n29^post2 == 0 /\ -ret18^post2+ret18^0 == 0 /\ -ret_fn132^post1+tmp___2^post1 == 0 /\ ret_fn144^0-ret_fn144^post2 == 0 /\ -tmp___5^post1+i7^post1 == 0 /\ ret26^0-ret26^post2 == 0 /\ -ret42^post1+ret_fn144^post1 == 0 /\ -tmp19^post2+tmp19^0 == 0 /\ ret34^post1-tmp35^post1 == 0 /\ -ret_fn140^post1+tmp___4^post1 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ ret22^post1-tmp23^post1 == 0 /\ -tmp___3^post2+tmp___3^0 == 0 /\ -n33^post2+n33^0 == 0 /\ i4^post1-tmp___2^post1 == 0 /\ n17^0-n17^post2 == 0 /\ -i2^post2+i2^0 == 0 /\ -tmp31^post2+tmp31^0 == 0 /\ tmp27^0-tmp27^post2 == 0 /\ -ret_fn128^post1+tmp___1^post1 == 0 /\ -2+n17^post1 == 0 /\ -n21^post2+n21^0 == 0 /\ ret42^post1-tmp43^post1 == 0 /\ tmp35^0-tmp35^post2 == 0 /\ -i1^post2+i1^0 == 0 /\ -2+n41^post1 == 0 /\ i1^post1-tmp^post1 == 0 /\ -ret42^post2+ret42^0 == 0 /\ ret34^0-ret34^post2 == 0 /\ ret_fn140^post1-ret38^post1 == 0), cost: 1 Applied deletion Removed the following rules: 0 1 Simplified Transitions Start location: l2 Program variables: i1^0 i2^0 i3^0 i4^0 i5^0 i6^0 i7^0 i8^0 n17^0 n21^0 n25^0 n29^0 n33^0 n37^0 n41^0 n45^0 ret18^0 ret22^0 ret26^0 ret30^0 ret34^0 ret38^0 ret42^0 ret46^0 ret_fn120^0 ret_fn124^0 ret_fn128^0 ret_fn132^0 ret_fn136^0 ret_fn140^0 ret_fn144^0 ret_fn148^0 tmp19^0 tmp23^0 tmp27^0 tmp31^0 tmp35^0 tmp39^0 tmp43^0 tmp47^0 tmp^0 tmp___0^0 tmp___1^0 tmp___2^0 tmp___3^0 tmp___4^0 tmp___5^0 tmp___6^0 3: l2 -> l1 : i1^0'=tmp^post1, i2^0'=tmp___0^post1, i3^0'=tmp___1^post1, i4^0'=tmp___2^post1, i5^0'=tmp___3^post1, i6^0'=tmp___4^post1, i7^0'=tmp___5^post1, i8^0'=tmp___6^post1, n17^0'=2, n21^0'=2, n25^0'=2, n29^0'=2, n33^0'=2, n37^0'=2, n41^0'=2, n45^0'=2, ret18^0'=tmp^post1, ret22^0'=tmp___0^post1, ret26^0'=tmp___1^post1, ret30^0'=tmp___2^post1, ret34^0'=tmp___3^post1, ret38^0'=tmp___4^post1, ret42^0'=tmp___5^post1, ret46^0'=tmp___6^post1, ret_fn120^0'=tmp^post1, ret_fn124^0'=tmp___0^post1, ret_fn128^0'=tmp___1^post1, ret_fn132^0'=tmp___2^post1, ret_fn136^0'=tmp___3^post1, ret_fn140^0'=tmp___4^post1, ret_fn144^0'=tmp___5^post1, ret_fn148^0'=tmp___6^post1, tmp19^0'=tmp^post1, tmp23^0'=tmp___0^post1, tmp27^0'=tmp___1^post1, tmp31^0'=tmp___2^post1, tmp35^0'=tmp___3^post1, tmp39^0'=tmp___4^post1, tmp43^0'=tmp___5^post1, tmp47^0'=tmp___6^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, tmp___2^0'=tmp___2^post1, tmp___3^0'=tmp___3^post1, tmp___4^0'=tmp___4^post1, tmp___5^0'=tmp___5^post1, tmp___6^0'=tmp___6^post1, T, cost: 1 Propagated Equalities Original rule: l2 -> l1 : i1^0'=i1^post1, i2^0'=i2^post1, i3^0'=i3^post1, i4^0'=i4^post1, i5^0'=i5^post1, i6^0'=i6^post1, i7^0'=i7^post1, i8^0'=i8^post1, n17^0'=n17^post1, n21^0'=n21^post1, n25^0'=n25^post1, n29^0'=n29^post1, n33^0'=n33^post1, n37^0'=n37^post1, n41^0'=n41^post1, n45^0'=n45^post1, ret18^0'=ret18^post1, ret22^0'=ret22^post1, ret26^0'=ret26^post1, ret30^0'=ret30^post1, ret34^0'=ret34^post1, ret38^0'=ret38^post1, ret42^0'=ret42^post1, ret46^0'=ret46^post1, ret_fn120^0'=ret_fn120^post1, ret_fn124^0'=ret_fn124^post1, ret_fn128^0'=ret_fn128^post1, ret_fn132^0'=ret_fn132^post1, ret_fn136^0'=ret_fn136^post1, ret_fn140^0'=ret_fn140^post1, ret_fn144^0'=ret_fn144^post1, ret_fn148^0'=ret_fn148^post1, tmp19^0'=tmp19^post1, tmp23^0'=tmp23^post1, tmp27^0'=tmp27^post1, tmp31^0'=tmp31^post1, tmp35^0'=tmp35^post1, tmp39^0'=tmp39^post1, tmp43^0'=tmp43^post1, tmp47^0'=tmp47^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, tmp___2^0'=tmp___2^post1, tmp___3^0'=tmp___3^post1, tmp___4^0'=tmp___4^post1, tmp___5^0'=tmp___5^post1, tmp___6^0'=tmp___6^post1, (0 == 0 /\ tmp47^0-tmp47^post2 == 0 /\ -2+n29^post1 == 0 /\ -n25^post2+n25^0 == 0 /\ -ret_fn148^post1+tmp___6^post1 == 0 /\ -n45^post2+n45^0 == 0 /\ -tmp___6^post1+i8^post1 == 0 /\ n41^0-n41^post2 == 0 /\ ret38^0-ret38^post2 == 0 /\ ret_fn128^post1-ret26^post1 == 0 /\ -ret_fn124^post2+ret_fn124^0 == 0 /\ ret_fn132^0-ret_fn132^post2 == 0 /\ ret18^post1-tmp19^post1 == 0 /\ -ret22^post1+ret_fn124^post1 == 0 /\ -2+n33^post1 == 0 /\ tmp23^0-tmp23^post2 == 0 /\ -i3^post2+i3^0 == 0 /\ -i8^post2+i8^0 == 0 /\ -tmp___0^post1+i2^post1 == 0 /\ -ret_fn128^post2+ret_fn128^0 == 0 /\ -2+n21^post1 == 0 /\ -n37^post2+n37^0 == 0 /\ tmp39^0-tmp39^post2 == 0 /\ -i5^post2+i5^0 == 0 /\ -2+n45^post1 == 0 /\ -ret_fn148^post2+ret_fn148^0 == 0 /\ ret38^post1-tmp39^post1 == 0 /\ -tmp___4^post1+i6^post1 == 0 /\ -tmp43^post2+tmp43^0 == 0 /\ -tmp___1^post1+i3^post1 == 0 /\ ret_fn136^post1-ret34^post1 == 0 /\ tmp___0^post1-ret_fn124^post1 == 0 /\ -tmp___5^post2+tmp___5^0 == 0 /\ -i6^post2+i6^0 == 0 /\ -ret30^post1+ret_fn132^post1 == 0 /\ -tmp___4^post2+tmp___4^0 == 0 /\ -ret30^post2+ret30^0 == 0 /\ ret46^post1-tmp47^post1 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___3^post1+i5^post1 == 0 /\ ret_fn148^post1-ret46^post1 == 0 /\ -tmp27^post1+ret26^post1 == 0 /\ ret_fn120^0-ret_fn120^post2 == 0 /\ -tmp___6^post2+tmp___6^0 == 0 /\ ret22^0-ret22^post2 == 0 /\ tmp___2^0-tmp___2^post2 == 0 /\ -ret18^post1+ret_fn120^post1 == 0 /\ -2+n37^post1 == 0 /\ -i7^post2+i7^0 == 0 /\ -ret_fn120^post1+tmp^post1 == 0 /\ -i4^post2+i4^0 == 0 /\ ret_fn140^0-ret_fn140^post2 == 0 /\ -ret_fn136^post1+tmp___3^post1 == 0 /\ -ret_fn136^post2+ret_fn136^0 == 0 /\ ret30^post1-tmp31^post1 == 0 /\ -2+n25^post1 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ -ret_fn144^post1+tmp___5^post1 == 0 /\ ret46^0-ret46^post2 == 0 /\ n29^0-n29^post2 == 0 /\ -ret18^post2+ret18^0 == 0 /\ -ret_fn132^post1+tmp___2^post1 == 0 /\ ret_fn144^0-ret_fn144^post2 == 0 /\ -tmp___5^post1+i7^post1 == 0 /\ ret26^0-ret26^post2 == 0 /\ -ret42^post1+ret_fn144^post1 == 0 /\ -tmp19^post2+tmp19^0 == 0 /\ ret34^post1-tmp35^post1 == 0 /\ -ret_fn140^post1+tmp___4^post1 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ ret22^post1-tmp23^post1 == 0 /\ -tmp___3^post2+tmp___3^0 == 0 /\ -n33^post2+n33^0 == 0 /\ i4^post1-tmp___2^post1 == 0 /\ n17^0-n17^post2 == 0 /\ -i2^post2+i2^0 == 0 /\ -tmp31^post2+tmp31^0 == 0 /\ tmp27^0-tmp27^post2 == 0 /\ -ret_fn128^post1+tmp___1^post1 == 0 /\ -2+n17^post1 == 0 /\ -n21^post2+n21^0 == 0 /\ ret42^post1-tmp43^post1 == 0 /\ tmp35^0-tmp35^post2 == 0 /\ -i1^post2+i1^0 == 0 /\ -2+n41^post1 == 0 /\ i1^post1-tmp^post1 == 0 /\ -ret42^post2+ret42^0 == 0 /\ ret34^0-ret34^post2 == 0 /\ ret_fn140^post1-ret38^post1 == 0), cost: 1 New rule: l2 -> l1 : i1^0'=tmp^post1, i2^0'=tmp___0^post1, i3^0'=tmp___1^post1, i4^0'=tmp___2^post1, i5^0'=tmp___3^post1, i6^0'=tmp___4^post1, i7^0'=tmp___5^post1, i8^0'=tmp___6^post1, n17^0'=2, n21^0'=2, n25^0'=2, n29^0'=2, n33^0'=2, n37^0'=2, n41^0'=2, n45^0'=2, ret18^0'=tmp^post1, ret22^0'=tmp___0^post1, ret26^0'=tmp___1^post1, ret30^0'=tmp___2^post1, ret34^0'=tmp___3^post1, ret38^0'=tmp___4^post1, ret42^0'=tmp___5^post1, ret46^0'=tmp___6^post1, ret_fn120^0'=tmp^post1, ret_fn124^0'=tmp___0^post1, ret_fn128^0'=tmp___1^post1, ret_fn132^0'=tmp___2^post1, ret_fn136^0'=tmp___3^post1, ret_fn140^0'=tmp___4^post1, ret_fn144^0'=tmp___5^post1, ret_fn148^0'=tmp___6^post1, tmp19^0'=tmp^post1, tmp23^0'=tmp___0^post1, tmp27^0'=tmp___1^post1, tmp31^0'=tmp___2^post1, tmp35^0'=tmp___3^post1, tmp39^0'=tmp___4^post1, tmp43^0'=tmp___5^post1, tmp47^0'=tmp___6^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, tmp___2^0'=tmp___2^post1, tmp___3^0'=tmp___3^post1, tmp___4^0'=tmp___4^post1, tmp___5^0'=tmp___5^post1, tmp___6^0'=tmp___6^post1, (0 == 0 /\ tmp47^0-tmp47^post2 == 0 /\ -n25^post2+n25^0 == 0 /\ -n45^post2+n45^0 == 0 /\ n41^0-n41^post2 == 0 /\ ret38^0-ret38^post2 == 0 /\ -ret_fn124^post2+ret_fn124^0 == 0 /\ ret_fn132^0-ret_fn132^post2 == 0 /\ tmp23^0-tmp23^post2 == 0 /\ -i3^post2+i3^0 == 0 /\ -i8^post2+i8^0 == 0 /\ -ret_fn128^post2+ret_fn128^0 == 0 /\ -n37^post2+n37^0 == 0 /\ tmp39^0-tmp39^post2 == 0 /\ -i5^post2+i5^0 == 0 /\ -ret_fn148^post2+ret_fn148^0 == 0 /\ -tmp43^post2+tmp43^0 == 0 /\ -tmp___5^post2+tmp___5^0 == 0 /\ -i6^post2+i6^0 == 0 /\ -tmp___4^post2+tmp___4^0 == 0 /\ -ret30^post2+ret30^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ ret_fn120^0-ret_fn120^post2 == 0 /\ -tmp___6^post2+tmp___6^0 == 0 /\ ret22^0-ret22^post2 == 0 /\ tmp___2^0-tmp___2^post2 == 0 /\ -i7^post2+i7^0 == 0 /\ -i4^post2+i4^0 == 0 /\ ret_fn140^0-ret_fn140^post2 == 0 /\ -ret_fn136^post2+ret_fn136^0 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ ret46^0-ret46^post2 == 0 /\ n29^0-n29^post2 == 0 /\ -ret18^post2+ret18^0 == 0 /\ ret_fn144^0-ret_fn144^post2 == 0 /\ ret26^0-ret26^post2 == 0 /\ -tmp19^post2+tmp19^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ -tmp___3^post2+tmp___3^0 == 0 /\ -n33^post2+n33^0 == 0 /\ n17^0-n17^post2 == 0 /\ -i2^post2+i2^0 == 0 /\ -tmp31^post2+tmp31^0 == 0 /\ tmp27^0-tmp27^post2 == 0 /\ -n21^post2+n21^0 == 0 /\ tmp35^0-tmp35^post2 == 0 /\ -i1^post2+i1^0 == 0 /\ -ret42^post2+ret42^0 == 0 /\ ret34^0-ret34^post2 == 0), cost: 1 propagated equality n29^post1 = 2 propagated equality ret_fn148^post1 = tmp___6^post1 propagated equality i8^post1 = tmp___6^post1 propagated equality ret26^post1 = ret_fn128^post1 propagated equality ret18^post1 = tmp19^post1 propagated equality ret22^post1 = ret_fn124^post1 propagated equality n33^post1 = 2 propagated equality i2^post1 = tmp___0^post1 propagated equality n21^post1 = 2 propagated equality n45^post1 = 2 propagated equality ret38^post1 = tmp39^post1 propagated equality i6^post1 = tmp___4^post1 propagated equality i3^post1 = tmp___1^post1 propagated equality ret34^post1 = ret_fn136^post1 propagated equality ret_fn124^post1 = tmp___0^post1 propagated equality ret30^post1 = ret_fn132^post1 propagated equality ret46^post1 = tmp47^post1 propagated equality i5^post1 = tmp___3^post1 propagated equality tmp47^post1 = tmp___6^post1 propagated equality ret_fn128^post1 = tmp27^post1 propagated equality ret_fn120^post1 = tmp19^post1 propagated equality n37^post1 = 2 propagated equality tmp19^post1 = tmp^post1 propagated equality ret_fn136^post1 = tmp___3^post1 propagated equality ret_fn132^post1 = tmp31^post1 propagated equality n25^post1 = 2 propagated equality ret_fn144^post1 = tmp___5^post1 propagated equality tmp31^post1 = tmp___2^post1 propagated equality i7^post1 = tmp___5^post1 propagated equality ret42^post1 = tmp___5^post1 propagated equality tmp35^post1 = tmp___3^post1 propagated equality ret_fn140^post1 = tmp___4^post1 propagated equality tmp23^post1 = tmp___0^post1 propagated equality i4^post1 = tmp___2^post1 propagated equality tmp27^post1 = tmp___1^post1 propagated equality n17^post1 = 2 propagated equality tmp43^post1 = tmp___5^post1 propagated equality n41^post1 = 2 propagated equality i1^post1 = tmp^post1 propagated equality tmp39^post1 = tmp___4^post1 Propagated Equalities Original rule: l2 -> l1 : i1^0'=tmp^post1, i2^0'=tmp___0^post1, i3^0'=tmp___1^post1, i4^0'=tmp___2^post1, i5^0'=tmp___3^post1, i6^0'=tmp___4^post1, i7^0'=tmp___5^post1, i8^0'=tmp___6^post1, n17^0'=2, n21^0'=2, n25^0'=2, n29^0'=2, n33^0'=2, n37^0'=2, n41^0'=2, n45^0'=2, ret18^0'=tmp^post1, ret22^0'=tmp___0^post1, ret26^0'=tmp___1^post1, ret30^0'=tmp___2^post1, ret34^0'=tmp___3^post1, ret38^0'=tmp___4^post1, ret42^0'=tmp___5^post1, ret46^0'=tmp___6^post1, ret_fn120^0'=tmp^post1, ret_fn124^0'=tmp___0^post1, ret_fn128^0'=tmp___1^post1, ret_fn132^0'=tmp___2^post1, ret_fn136^0'=tmp___3^post1, ret_fn140^0'=tmp___4^post1, ret_fn144^0'=tmp___5^post1, ret_fn148^0'=tmp___6^post1, tmp19^0'=tmp^post1, tmp23^0'=tmp___0^post1, tmp27^0'=tmp___1^post1, tmp31^0'=tmp___2^post1, tmp35^0'=tmp___3^post1, tmp39^0'=tmp___4^post1, tmp43^0'=tmp___5^post1, tmp47^0'=tmp___6^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, tmp___2^0'=tmp___2^post1, tmp___3^0'=tmp___3^post1, tmp___4^0'=tmp___4^post1, tmp___5^0'=tmp___5^post1, tmp___6^0'=tmp___6^post1, (0 == 0 /\ tmp47^0-tmp47^post2 == 0 /\ -n25^post2+n25^0 == 0 /\ -n45^post2+n45^0 == 0 /\ n41^0-n41^post2 == 0 /\ ret38^0-ret38^post2 == 0 /\ -ret_fn124^post2+ret_fn124^0 == 0 /\ ret_fn132^0-ret_fn132^post2 == 0 /\ tmp23^0-tmp23^post2 == 0 /\ -i3^post2+i3^0 == 0 /\ -i8^post2+i8^0 == 0 /\ -ret_fn128^post2+ret_fn128^0 == 0 /\ -n37^post2+n37^0 == 0 /\ tmp39^0-tmp39^post2 == 0 /\ -i5^post2+i5^0 == 0 /\ -ret_fn148^post2+ret_fn148^0 == 0 /\ -tmp43^post2+tmp43^0 == 0 /\ -tmp___5^post2+tmp___5^0 == 0 /\ -i6^post2+i6^0 == 0 /\ -tmp___4^post2+tmp___4^0 == 0 /\ -ret30^post2+ret30^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ ret_fn120^0-ret_fn120^post2 == 0 /\ -tmp___6^post2+tmp___6^0 == 0 /\ ret22^0-ret22^post2 == 0 /\ tmp___2^0-tmp___2^post2 == 0 /\ -i7^post2+i7^0 == 0 /\ -i4^post2+i4^0 == 0 /\ ret_fn140^0-ret_fn140^post2 == 0 /\ -ret_fn136^post2+ret_fn136^0 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ ret46^0-ret46^post2 == 0 /\ n29^0-n29^post2 == 0 /\ -ret18^post2+ret18^0 == 0 /\ ret_fn144^0-ret_fn144^post2 == 0 /\ ret26^0-ret26^post2 == 0 /\ -tmp19^post2+tmp19^0 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ -tmp___3^post2+tmp___3^0 == 0 /\ -n33^post2+n33^0 == 0 /\ n17^0-n17^post2 == 0 /\ -i2^post2+i2^0 == 0 /\ -tmp31^post2+tmp31^0 == 0 /\ tmp27^0-tmp27^post2 == 0 /\ -n21^post2+n21^0 == 0 /\ tmp35^0-tmp35^post2 == 0 /\ -i1^post2+i1^0 == 0 /\ -ret42^post2+ret42^0 == 0 /\ ret34^0-ret34^post2 == 0), cost: 1 New rule: l2 -> l1 : i1^0'=tmp^post1, i2^0'=tmp___0^post1, i3^0'=tmp___1^post1, i4^0'=tmp___2^post1, i5^0'=tmp___3^post1, i6^0'=tmp___4^post1, i7^0'=tmp___5^post1, i8^0'=tmp___6^post1, n17^0'=2, n21^0'=2, n25^0'=2, n29^0'=2, n33^0'=2, n37^0'=2, n41^0'=2, n45^0'=2, ret18^0'=tmp^post1, ret22^0'=tmp___0^post1, ret26^0'=tmp___1^post1, ret30^0'=tmp___2^post1, ret34^0'=tmp___3^post1, ret38^0'=tmp___4^post1, ret42^0'=tmp___5^post1, ret46^0'=tmp___6^post1, ret_fn120^0'=tmp^post1, ret_fn124^0'=tmp___0^post1, ret_fn128^0'=tmp___1^post1, ret_fn132^0'=tmp___2^post1, ret_fn136^0'=tmp___3^post1, ret_fn140^0'=tmp___4^post1, ret_fn144^0'=tmp___5^post1, ret_fn148^0'=tmp___6^post1, tmp19^0'=tmp^post1, tmp23^0'=tmp___0^post1, tmp27^0'=tmp___1^post1, tmp31^0'=tmp___2^post1, tmp35^0'=tmp___3^post1, tmp39^0'=tmp___4^post1, tmp43^0'=tmp___5^post1, tmp47^0'=tmp___6^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, tmp___2^0'=tmp___2^post1, tmp___3^0'=tmp___3^post1, tmp___4^0'=tmp___4^post1, tmp___5^0'=tmp___5^post1, tmp___6^0'=tmp___6^post1, 0 == 0, cost: 1 propagated equality tmp47^post2 = tmp47^0 propagated equality n25^post2 = n25^0 propagated equality n45^post2 = n45^0 propagated equality n41^post2 = n41^0 propagated equality ret38^post2 = ret38^0 propagated equality ret_fn124^post2 = ret_fn124^0 propagated equality ret_fn132^post2 = ret_fn132^0 propagated equality tmp23^post2 = tmp23^0 propagated equality i3^post2 = i3^0 propagated equality i8^post2 = i8^0 propagated equality ret_fn128^post2 = ret_fn128^0 propagated equality n37^post2 = n37^0 propagated equality tmp39^post2 = tmp39^0 propagated equality i5^post2 = i5^0 propagated equality ret_fn148^post2 = ret_fn148^0 propagated equality tmp43^post2 = tmp43^0 propagated equality tmp___5^post2 = tmp___5^0 propagated equality i6^post2 = i6^0 propagated equality tmp___4^post2 = tmp___4^0 propagated equality ret30^post2 = ret30^0 propagated equality tmp^post2 = tmp^0 propagated equality ret_fn120^post2 = ret_fn120^0 propagated equality tmp___6^post2 = tmp___6^0 propagated equality ret22^post2 = ret22^0 propagated equality tmp___2^post2 = tmp___2^0 propagated equality i7^post2 = i7^0 propagated equality i4^post2 = i4^0 propagated equality ret_fn140^post2 = ret_fn140^0 propagated equality ret_fn136^post2 = ret_fn136^0 propagated equality tmp___1^post2 = tmp___1^0 propagated equality ret46^post2 = ret46^0 propagated equality n29^post2 = n29^0 propagated equality ret18^post2 = ret18^0 propagated equality ret_fn144^post2 = ret_fn144^0 propagated equality ret26^post2 = ret26^0 propagated equality tmp19^post2 = tmp19^0 propagated equality tmp___0^post2 = tmp___0^0 propagated equality tmp___3^post2 = tmp___3^0 propagated equality n33^post2 = n33^0 propagated equality n17^post2 = n17^0 propagated equality i2^post2 = i2^0 propagated equality tmp31^post2 = tmp31^0 propagated equality tmp27^post2 = tmp27^0 propagated equality n21^post2 = n21^0 propagated equality tmp35^post2 = tmp35^0 propagated equality i1^post2 = i1^0 propagated equality ret42^post2 = ret42^0 propagated equality ret34^post2 = ret34^0 Simplified Guard Original rule: l2 -> l1 : i1^0'=tmp^post1, i2^0'=tmp___0^post1, i3^0'=tmp___1^post1, i4^0'=tmp___2^post1, i5^0'=tmp___3^post1, i6^0'=tmp___4^post1, i7^0'=tmp___5^post1, i8^0'=tmp___6^post1, n17^0'=2, n21^0'=2, n25^0'=2, n29^0'=2, n33^0'=2, n37^0'=2, n41^0'=2, n45^0'=2, ret18^0'=tmp^post1, ret22^0'=tmp___0^post1, ret26^0'=tmp___1^post1, ret30^0'=tmp___2^post1, ret34^0'=tmp___3^post1, ret38^0'=tmp___4^post1, ret42^0'=tmp___5^post1, ret46^0'=tmp___6^post1, ret_fn120^0'=tmp^post1, ret_fn124^0'=tmp___0^post1, ret_fn128^0'=tmp___1^post1, ret_fn132^0'=tmp___2^post1, ret_fn136^0'=tmp___3^post1, ret_fn140^0'=tmp___4^post1, ret_fn144^0'=tmp___5^post1, ret_fn148^0'=tmp___6^post1, tmp19^0'=tmp^post1, tmp23^0'=tmp___0^post1, tmp27^0'=tmp___1^post1, tmp31^0'=tmp___2^post1, tmp35^0'=tmp___3^post1, tmp39^0'=tmp___4^post1, tmp43^0'=tmp___5^post1, tmp47^0'=tmp___6^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, tmp___2^0'=tmp___2^post1, tmp___3^0'=tmp___3^post1, tmp___4^0'=tmp___4^post1, tmp___5^0'=tmp___5^post1, tmp___6^0'=tmp___6^post1, 0 == 0, cost: 1 New rule: l2 -> l1 : i1^0'=tmp^post1, i2^0'=tmp___0^post1, i3^0'=tmp___1^post1, i4^0'=tmp___2^post1, i5^0'=tmp___3^post1, i6^0'=tmp___4^post1, i7^0'=tmp___5^post1, i8^0'=tmp___6^post1, n17^0'=2, n21^0'=2, n25^0'=2, n29^0'=2, n33^0'=2, n37^0'=2, n41^0'=2, n45^0'=2, ret18^0'=tmp^post1, ret22^0'=tmp___0^post1, ret26^0'=tmp___1^post1, ret30^0'=tmp___2^post1, ret34^0'=tmp___3^post1, ret38^0'=tmp___4^post1, ret42^0'=tmp___5^post1, ret46^0'=tmp___6^post1, ret_fn120^0'=tmp^post1, ret_fn124^0'=tmp___0^post1, ret_fn128^0'=tmp___1^post1, ret_fn132^0'=tmp___2^post1, ret_fn136^0'=tmp___3^post1, ret_fn140^0'=tmp___4^post1, ret_fn144^0'=tmp___5^post1, ret_fn148^0'=tmp___6^post1, tmp19^0'=tmp^post1, tmp23^0'=tmp___0^post1, tmp27^0'=tmp___1^post1, tmp31^0'=tmp___2^post1, tmp35^0'=tmp___3^post1, tmp39^0'=tmp___4^post1, tmp43^0'=tmp___5^post1, tmp47^0'=tmp___6^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, tmp___2^0'=tmp___2^post1, tmp___3^0'=tmp___3^post1, tmp___4^0'=tmp___4^post1, tmp___5^0'=tmp___5^post1, tmp___6^0'=tmp___6^post1, T, cost: 1 Step with 3 Trace 3[T] Blocked [{}, {}] Backtrack Trace Blocked [{3[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b