NO Initial ITS Start location: l13 0: l0 -> l1 : a1111^0'=a1111^post0, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post0, i^0'=i^post0, PdoType^0'=PdoType^post0, num^0'=num^post0, c33^0'=c33^post0, unset^0'=unset^post0, status^0'=status^post0, a77^0'=a77^post0, Pdolen^0'=Pdolen^post0, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post0, dcIdi^0'=dcIdi^post0, tmp99^0'=tmp99^post0, DName^0'=DName^post0, b22^0'=b22^post0, a11^0'=a11^post0, set^0'=set^post0, lptNamei^0'=lptNamei^post0, Pdoi^0'=Pdoi^post0, pc^0'=pc^post0, d44^0'=d44^post0, tmp55^0'=tmp55^post0, a88^0'=a88^post0, (dcIdi^0-dcIdi^post0 == 0 /\ pc^0-pc^post0 == 0 /\ -a77^post0+a77^0 == 0 /\ -a88^post0+a88^0 == 0 /\ -lptNamei^post0+lptNamei^0 == 0 /\ status^0-status^post0 == 0 /\ -unset^post0+unset^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post0 == 0 /\ -d44^post0+d44^0 == 0 /\ -tmp55^post0+tmp55^0 == 0 /\ -Pdolen^post0+Pdolen^0 == 0 /\ -Pdoi^post0+Pdoi^0 == 0 /\ -ret_IoCreateDevice1010^post0+ret_IoCreateDevice1010^0 == 0 /\ tmp99^0-tmp99^post0 == 0 /\ i^0-i^post0 == 0 /\ set^0-set^post0 == 0 /\ c33^0-c33^post0 == 0 /\ -DName^post0+DName^0 == 0 /\ b22^0-b22^post0 == 0 /\ a11^0-a11^post0 == 0 /\ num^0-num^post0 == 0 /\ a1111^0-a1111^post0 == 0 /\ PdoType^0-PdoType^post0 == 0), cost: 1 1: l2 -> l3 : a1111^0'=a1111^post1, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post1, i^0'=i^post1, PdoType^0'=PdoType^post1, num^0'=num^post1, c33^0'=c33^post1, unset^0'=unset^post1, status^0'=status^post1, a77^0'=a77^post1, Pdolen^0'=Pdolen^post1, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post1, dcIdi^0'=dcIdi^post1, tmp99^0'=tmp99^post1, DName^0'=DName^post1, b22^0'=b22^post1, a11^0'=a11^post1, set^0'=set^post1, lptNamei^0'=lptNamei^post1, Pdoi^0'=Pdoi^post1, pc^0'=pc^post1, d44^0'=d44^post1, tmp55^0'=tmp55^post1, a88^0'=a88^post1, (unset^post1 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post1 == 0 /\ tmp99^0-tmp99^post1 == 0 /\ -1+unset^10 == 0 /\ -lptNamei^post1+lptNamei^0 == 0 /\ dcIdi^0-dcIdi^post1 == 0 /\ -pc^post1+pc^0 == 0 /\ a1111^0-a1111^post1 == 0 /\ -ret_IoCreateDevice1010^post1+ret_IoCreateDevice1010^0 == 0 /\ PdoType^0-PdoType^post1 == 0 /\ Pdolen^0-Pdolen^post1 == 0 /\ -Pdoi^post1+Pdoi^0 == 0 /\ set^0-set^post1 == 0 /\ -status^post1+status^0 == 0 /\ -tmp55^post1+tmp55^0 == 0 /\ num^post1 == 0 /\ -a88^post1+a88^0 == 0 /\ a11^0-a11^post1 == 0 /\ -DName^post1+DName^0 == 0 /\ -b22^post1+b22^0 == 0 /\ -i^post1+i^0 == 0 /\ a77^0-a77^post1 == 0 /\ c33^0-c33^post1 == 0 /\ -d44^post1+d44^0 == 0), cost: 1 13: l3 -> l11 : a1111^0'=a1111^post13, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post13, i^0'=i^post13, PdoType^0'=PdoType^post13, num^0'=num^post13, c33^0'=c33^post13, unset^0'=unset^post13, status^0'=status^post13, a77^0'=a77^post13, Pdolen^0'=Pdolen^post13, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post13, dcIdi^0'=dcIdi^post13, tmp99^0'=tmp99^post13, DName^0'=DName^post13, b22^0'=b22^post13, a11^0'=a11^post13, set^0'=set^post13, lptNamei^0'=lptNamei^post13, Pdoi^0'=Pdoi^post13, pc^0'=pc^post13, d44^0'=d44^post13, tmp55^0'=tmp55^post13, a88^0'=a88^post13, (-a77^post13+a77^0 == 0 /\ -d44^post13+d44^0 == 0 /\ -a88^post13+a88^0 == 0 /\ Pdoi^0-Pdoi^post13 == 0 /\ i^0-i^post13 == 0 /\ -tmp55^post13+tmp55^0 == 0 /\ unset^0-unset^post13 == 0 /\ -Pdolen^post13+Pdolen^0 == 0 /\ -lptNamei^post13+lptNamei^0 == 0 /\ a1111^0-a1111^post13 == 0 /\ -set^post13+set^0 == 0 /\ b22^0-b22^post13 == 0 /\ PdoType^0-PdoType^post13 == 0 /\ dcIdi^0-dcIdi^post13 == 0 /\ status^0-status^post13 == 0 /\ -ret_IoCreateDevice1010^post13+ret_IoCreateDevice1010^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post13 == 0 /\ -num^post13+num^0 == 0 /\ -pc^post13+pc^0 == 0 /\ a11^0-a11^post13 == 0 /\ -c33^post13+c33^0 == 0 /\ -tmp99^post13+tmp99^0 == 0 /\ -DName^post13+DName^0 == 0), cost: 1 2: l4 -> l2 : a1111^0'=a1111^post2, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post2, i^0'=i^post2, PdoType^0'=PdoType^post2, num^0'=num^post2, c33^0'=c33^post2, unset^0'=unset^post2, status^0'=status^post2, a77^0'=a77^post2, Pdolen^0'=Pdolen^post2, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post2, dcIdi^0'=dcIdi^post2, tmp99^0'=tmp99^post2, DName^0'=DName^post2, b22^0'=b22^post2, a11^0'=a11^post2, set^0'=set^post2, lptNamei^0'=lptNamei^post2, Pdoi^0'=Pdoi^post2, pc^0'=pc^post2, d44^0'=d44^post2, tmp55^0'=tmp55^post2, a88^0'=a88^post2, (-set^post2+set^0 == 0 /\ -DName^post2+DName^0 == 0 /\ PdoType^0-PdoType^post2 == 0 /\ a1111^0-a1111^post2 == 0 /\ -ret_IoCreateDevice1010^post2+ret_IoCreateDevice1010^0 == 0 /\ -pc^post2+pc^0 == 0 /\ -Pdoi^post2+Pdoi^0 == 0 /\ status^0-status^post2 == 0 /\ i^0-i^post2 == 0 /\ tmp99^0-tmp99^post2 == 0 /\ -d44^post2+d44^0 == 0 /\ num^0-num^post2 == 0 /\ c33^0-c33^post2 == 0 /\ -a77^post2+a77^0 == 0 /\ b22^0-b22^post2 == 0 /\ -tmp55^post2+tmp55^0 == 0 /\ -unset^post2+unset^0 == 0 /\ a11^0-a11^post2 == 0 /\ dcIdi^0-dcIdi^post2 == 0 /\ Pdolen^0-Pdolen^post2 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post2 == 0 /\ -lptNamei^post2+lptNamei^0 == 0 /\ -a88^post2+a88^0 == 0), cost: 1 3: l5 -> l4 : a1111^0'=a1111^post3, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post3, i^0'=i^post3, PdoType^0'=PdoType^post3, num^0'=num^post3, c33^0'=c33^post3, unset^0'=unset^post3, status^0'=status^post3, a77^0'=a77^post3, Pdolen^0'=Pdolen^post3, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post3, dcIdi^0'=dcIdi^post3, tmp99^0'=tmp99^post3, DName^0'=DName^post3, b22^0'=b22^post3, a11^0'=a11^post3, set^0'=set^post3, lptNamei^0'=lptNamei^post3, Pdoi^0'=Pdoi^post3, pc^0'=pc^post3, d44^0'=d44^post3, tmp55^0'=tmp55^post3, a88^0'=a88^post3, (-a77^post3+a77^0 == 0 /\ -set^post3+set^0 == 0 /\ a1111^0-a1111^post3 == 0 /\ b22^0-b22^post3 == 0 /\ unset^0-unset^post3 == 0 /\ -pc^post3+pc^0 == 0 /\ -1+status^0 <= 0 /\ i^0-i^post3 == 0 /\ -DName^post3+DName^0 == 0 /\ PdoType^0-PdoType^post3 == 0 /\ dcIdi^0-dcIdi^post3 == 0 /\ status^0-status^post3 == 0 /\ -d44^post3+d44^0 == 0 /\ c33^0-c33^post3 == 0 /\ -a11^post3+a11^0 == 0 /\ -tmp55^post3+tmp55^0 == 0 /\ -tmp99^post3+tmp99^0 == 0 /\ -Pdolen^post3+Pdolen^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post3 == 0 /\ -Pdoi^post3+Pdoi^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post3 == 0 /\ -num^post3+num^0 == 0 /\ lptNamei^0-lptNamei^post3 == 0 /\ -a88^post3+a88^0 == 0), cost: 1 4: l5 -> l4 : a1111^0'=a1111^post4, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post4, i^0'=i^post4, PdoType^0'=PdoType^post4, num^0'=num^post4, c33^0'=c33^post4, unset^0'=unset^post4, status^0'=status^post4, a77^0'=a77^post4, Pdolen^0'=Pdolen^post4, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post4, dcIdi^0'=dcIdi^post4, tmp99^0'=tmp99^post4, DName^0'=DName^post4, b22^0'=b22^post4, a11^0'=a11^post4, set^0'=set^post4, lptNamei^0'=lptNamei^post4, Pdoi^0'=Pdoi^post4, pc^0'=pc^post4, d44^0'=d44^post4, tmp55^0'=tmp55^post4, a88^0'=a88^post4, (-a77^post4+a77^0 == 0 /\ -a88^post4+a88^0 == 0 /\ -a11^post4+a11^0 == 0 /\ Pdoi^0-Pdoi^post4 == 0 /\ -d44^post4+d44^0 == 0 /\ i^0-i^post4 == 0 /\ -tmp55^post4+tmp55^0 == 0 /\ unset^0-unset^post4 == 0 /\ -tmp99^post4+tmp99^0 == 0 /\ 3-status^0 <= 0 /\ b22^0-b22^post4 == 0 /\ a1111^0-a1111^post4 == 0 /\ PdoType^0-PdoType^post4 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post4 == 0 /\ lptNamei^0-lptNamei^post4 == 0 /\ dcIdi^0-dcIdi^post4 == 0 /\ status^0-status^post4 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post4 == 0 /\ -Pdolen^post4+Pdolen^0 == 0 /\ -num^post4+num^0 == 0 /\ -DName^post4+DName^0 == 0 /\ -pc^post4+pc^0 == 0 /\ -c33^post4+c33^0 == 0 /\ -set^post4+set^0 == 0), cost: 1 5: l5 -> l4 : a1111^0'=a1111^post5, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post5, i^0'=i^post5, PdoType^0'=PdoType^post5, num^0'=num^post5, c33^0'=c33^post5, unset^0'=unset^post5, status^0'=status^post5, a77^0'=a77^post5, Pdolen^0'=Pdolen^post5, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post5, dcIdi^0'=dcIdi^post5, tmp99^0'=tmp99^post5, DName^0'=DName^post5, b22^0'=b22^post5, a11^0'=a11^post5, set^0'=set^post5, lptNamei^0'=lptNamei^post5, Pdoi^0'=Pdoi^post5, pc^0'=pc^post5, d44^0'=d44^post5, tmp55^0'=tmp55^post5, a88^0'=a88^post5, (-dcIdi^post5+dcIdi^0 == 0 /\ b22^0-b22^post5 == 0 /\ -tmp99^post5+tmp99^0 == 0 /\ -tmp55^post5+tmp55^0 == 0 /\ 2-status^0 <= 0 /\ -Pdoi^post5+Pdoi^0 == 0 /\ -a11^post5+a11^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post5 == 0 /\ -d44^post5+d44^0 == 0 /\ -Pdolen^post5+Pdolen^0 == 0 /\ -a88^post5+a88^0 == 0 /\ -set^post5+set^0 == 0 /\ unset^0-unset^post5 == 0 /\ PdoType^0-PdoType^post5 == 0 /\ -a77^post5+a77^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post5 == 0 /\ lptNamei^0-lptNamei^post5 == 0 /\ -2+status^0 <= 0 /\ -1-num^0+num^post5 == 0 /\ i^0-i^post5 == 0 /\ -DName^post5+DName^0 == 0 /\ -DName^0+a1111^post5 == 0 /\ -pc^post5+pc^0 == 0 /\ status^0-status^post5 == 0 /\ c33^0-c33^post5 == 0), cost: 1 6: l6 -> l5 : a1111^0'=a1111^post6, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post6, i^0'=i^post6, PdoType^0'=PdoType^post6, num^0'=num^post6, c33^0'=c33^post6, unset^0'=unset^post6, status^0'=status^post6, a77^0'=a77^post6, Pdolen^0'=Pdolen^post6, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post6, dcIdi^0'=dcIdi^post6, tmp99^0'=tmp99^post6, DName^0'=DName^post6, b22^0'=b22^post6, a11^0'=a11^post6, set^0'=set^post6, lptNamei^0'=lptNamei^post6, Pdoi^0'=Pdoi^post6, pc^0'=pc^post6, d44^0'=d44^post6, tmp55^0'=tmp55^post6, a88^0'=a88^post6, (Pdoi^post6 == 0 /\ Pdolen^0-Pdolen^post6 == 0 /\ -dcIdi^post6+dcIdi^0 == 0 /\ -lptNamei^post6+lptNamei^0 == 0 /\ a77^0-a77^post6 == 0 /\ -a88^post6+a88^0 == 0 /\ -b22^post6+b22^0 == 0 /\ i^0-i^post6 == 0 /\ -d44^post6+d44^0 == 0 /\ -set^post6+set^0 == 0 /\ -tmp99^post6+tmp99^0 == 0 /\ status^0-status^post6 == 0 /\ -tmp55^post6+tmp55^0 == 0 /\ -pc^post6+pc^0 == 0 /\ c33^0-c33^post6 == 0 /\ -ret_PPMakeDeviceName66^post6+ret_PPMakeDeviceName66^0 == 0 /\ DName^0-DName^post6 == 0 /\ a1111^0-a1111^post6 == 0 /\ unset^0-unset^post6 == 0 /\ PdoType^0-PdoType^post6 == 0 /\ -a11^post6+a11^0 == 0 /\ num^0-num^post6 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post6 == 0), cost: 1 7: l7 -> l8 : a1111^0'=a1111^post7, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post7, i^0'=i^post7, PdoType^0'=PdoType^post7, num^0'=num^post7, c33^0'=c33^post7, unset^0'=unset^post7, status^0'=status^post7, a77^0'=a77^post7, Pdolen^0'=Pdolen^post7, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post7, dcIdi^0'=dcIdi^post7, tmp99^0'=tmp99^post7, DName^0'=DName^post7, b22^0'=b22^post7, a11^0'=a11^post7, set^0'=set^post7, lptNamei^0'=lptNamei^post7, Pdoi^0'=Pdoi^post7, pc^0'=pc^post7, d44^0'=d44^post7, tmp55^0'=tmp55^post7, a88^0'=a88^post7, (-ret_IoCreateDevice1010^post7+ret_IoCreateDevice1010^0 == 0 /\ -pc^post7+pc^0 == 0 /\ a1111^0-a1111^post7 == 0 /\ unset^0-unset^post7 == 0 /\ -set^post7+set^0 == 0 /\ -status^post7+status^0 == 0 /\ Pdolen^0-Pdolen^post7 == 0 /\ DName^0-DName^post7 == 0 /\ -b22^post7+b22^0 == 0 /\ c33^0-c33^post7 == 0 /\ 1-status^0 <= 0 /\ -1+status^0 <= 0 /\ -d44^post7+d44^0 == 0 /\ -Pdoi^post7+Pdoi^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post7 == 0 /\ -1-i^0+i^post7 == 0 /\ a77^0-a77^post7 == 0 /\ dcIdi^0-dcIdi^post7 == 0 /\ num^0-num^post7 == 0 /\ -a11^post7+a11^0 == 0 /\ -tmp55^post7+tmp55^0 == 0 /\ -PdoType^post7+PdoType^0 == 0 /\ -a88^post7+a88^0 == 0 /\ tmp99^0-tmp99^post7 == 0 /\ -lptNamei^post7+lptNamei^0 == 0), cost: 1 8: l7 -> l6 : a1111^0'=a1111^post8, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post8, i^0'=i^post8, PdoType^0'=PdoType^post8, num^0'=num^post8, c33^0'=c33^post8, unset^0'=unset^post8, status^0'=status^post8, a77^0'=a77^post8, Pdolen^0'=Pdolen^post8, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post8, dcIdi^0'=dcIdi^post8, tmp99^0'=tmp99^post8, DName^0'=DName^post8, b22^0'=b22^post8, a11^0'=a11^post8, set^0'=set^post8, lptNamei^0'=lptNamei^post8, Pdoi^0'=Pdoi^post8, pc^0'=pc^post8, d44^0'=d44^post8, tmp55^0'=tmp55^post8, a88^0'=a88^post8, (c33^0-c33^post8 == 0 /\ -PdoType^post8+PdoType^0 == 0 /\ -pc^post8+pc^0 == 0 /\ unset^0-unset^post8 == 0 /\ -status^post8+status^0 == 0 /\ -ret_IoCreateDevice1010^post8+ret_IoCreateDevice1010^0 == 0 /\ num^0-num^post8 == 0 /\ a11^0-a11^post8 == 0 /\ a1111^0-a1111^post8 == 0 /\ status^0 <= 0 /\ DName^0-DName^post8 == 0 /\ Pdolen^0-Pdolen^post8 == 0 /\ -tmp55^post8+tmp55^0 == 0 /\ -Pdoi^post8+Pdoi^0 == 0 /\ -b22^post8+b22^0 == 0 /\ a77^0-a77^post8 == 0 /\ dcIdi^0-dcIdi^post8 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post8 == 0 /\ i^0-i^post8 == 0 /\ tmp99^0-tmp99^post8 == 0 /\ -a88^post8+a88^0 == 0 /\ -lptNamei^post8+lptNamei^0 == 0 /\ -d44^post8+d44^0 == 0 /\ set^0-set^post8 == 0), cost: 1 9: l7 -> l6 : a1111^0'=a1111^post9, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post9, i^0'=i^post9, PdoType^0'=PdoType^post9, num^0'=num^post9, c33^0'=c33^post9, unset^0'=unset^post9, status^0'=status^post9, a77^0'=a77^post9, Pdolen^0'=Pdolen^post9, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post9, dcIdi^0'=dcIdi^post9, tmp99^0'=tmp99^post9, DName^0'=DName^post9, b22^0'=b22^post9, a11^0'=a11^post9, set^0'=set^post9, lptNamei^0'=lptNamei^post9, Pdoi^0'=Pdoi^post9, pc^0'=pc^post9, d44^0'=d44^post9, tmp55^0'=tmp55^post9, a88^0'=a88^post9, (pc^0-pc^post9 == 0 /\ dcIdi^0-dcIdi^post9 == 0 /\ -d44^post9+d44^0 == 0 /\ -a88^post9+a88^0 == 0 /\ -a77^post9+a77^0 == 0 /\ 2-status^0 <= 0 /\ -unset^post9+unset^0 == 0 /\ -Pdoi^post9+Pdoi^0 == 0 /\ tmp99^0-tmp99^post9 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post9 == 0 /\ -tmp55^post9+tmp55^0 == 0 /\ a11^0-a11^post9 == 0 /\ -lptNamei^post9+lptNamei^0 == 0 /\ Pdolen^0-Pdolen^post9 == 0 /\ -status^post9+status^0 == 0 /\ -DName^post9+DName^0 == 0 /\ i^0-i^post9 == 0 /\ -ret_IoCreateDevice1010^post9+ret_IoCreateDevice1010^0 == 0 /\ set^0-set^post9 == 0 /\ num^0-num^post9 == 0 /\ c33^0-c33^post9 == 0 /\ -b22^post9+b22^0 == 0 /\ a1111^0-a1111^post9 == 0 /\ PdoType^0-PdoType^post9 == 0), cost: 1 10: l8 -> l9 : a1111^0'=a1111^post10, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post10, i^0'=i^post10, PdoType^0'=PdoType^post10, num^0'=num^post10, c33^0'=c33^post10, unset^0'=unset^post10, status^0'=status^post10, a77^0'=a77^post10, Pdolen^0'=Pdolen^post10, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post10, dcIdi^0'=dcIdi^post10, tmp99^0'=tmp99^post10, DName^0'=DName^post10, b22^0'=b22^post10, a11^0'=a11^post10, set^0'=set^post10, lptNamei^0'=lptNamei^post10, Pdoi^0'=Pdoi^post10, pc^0'=pc^post10, d44^0'=d44^post10, tmp55^0'=tmp55^post10, a88^0'=a88^post10, (pc^0-pc^post10 == 0 /\ -lptNamei^post10+lptNamei^0 == 0 /\ -a88^post10+a88^0 == 0 /\ a1111^0-a1111^post10 == 0 /\ -d44^post10+d44^0 == 0 /\ PdoType^0-PdoType^post10 == 0 /\ -tmp55^post10+tmp55^0 == 0 /\ -Pdolen^post10+Pdolen^0 == 0 /\ -Pdoi^post10+Pdoi^0 == 0 /\ -ret_IoCreateDevice1010^post10+ret_IoCreateDevice1010^0 == 0 /\ tmp99^0-tmp99^post10 == 0 /\ status^0-status^post10 == 0 /\ -a77^post10+a77^0 == 0 /\ b22^0-b22^post10 == 0 /\ -unset^post10+unset^0 == 0 /\ num^0-num^post10 == 0 /\ i^0-i^post10 == 0 /\ set^0-set^post10 == 0 /\ a11^0-a11^post10 == 0 /\ c33^0-c33^post10 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post10 == 0 /\ -DName^post10+DName^0 == 0 /\ dcIdi^0-dcIdi^post10 == 0), cost: 1 15: l9 -> l10 : a1111^0'=a1111^post15, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post15, i^0'=i^post15, PdoType^0'=PdoType^post15, num^0'=num^post15, c33^0'=c33^post15, unset^0'=unset^post15, status^0'=status^post15, a77^0'=a77^post15, Pdolen^0'=Pdolen^post15, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post15, dcIdi^0'=dcIdi^post15, tmp99^0'=tmp99^post15, DName^0'=DName^post15, b22^0'=b22^post15, a11^0'=a11^post15, set^0'=set^post15, lptNamei^0'=lptNamei^post15, Pdoi^0'=Pdoi^post15, pc^0'=pc^post15, d44^0'=d44^post15, tmp55^0'=tmp55^post15, a88^0'=a88^post15, (0 == 0 /\ -dcIdi^post15+dcIdi^0 == 0 /\ ret_PPMakeDeviceName66^post15-tmp55^post15 == 0 /\ 1+i^0-Pdolen^0 <= 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post15 == 0 /\ -num^post15+num^0 == 0 /\ -Pdolen^post15+Pdolen^0 == 0 /\ Pdoi^0-Pdoi^post15 == 0 /\ -set^post15+set^0 == 0 /\ unset^0-unset^post15 == 0 /\ PdoType^0-PdoType^post15 == 0 /\ -a77^post15+a77^0 == 0 /\ -pc^post15+pc^0 == 0 /\ -tmp99^post15+tmp99^0 == 0 /\ -PdoType^0+b22^post15 == 0 /\ a1111^0-a1111^post15 == 0 /\ -a88^post15+a88^0 == 0 /\ DName^post15-ret_PPMakeDeviceName66^post15 == 0 /\ c33^post15-dcIdi^0 == 0 /\ -lptNamei^post15+lptNamei^0 == 0 /\ status^0-status^post15 == 0 /\ a11^post15-lptNamei^0 == 0 /\ i^0-i^post15 == 0 /\ -num^0+d44^post15 == 0), cost: 1 16: l9 -> l2 : a1111^0'=a1111^post16, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post16, i^0'=i^post16, PdoType^0'=PdoType^post16, num^0'=num^post16, c33^0'=c33^post16, unset^0'=unset^post16, status^0'=status^post16, a77^0'=a77^post16, Pdolen^0'=Pdolen^post16, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post16, dcIdi^0'=dcIdi^post16, tmp99^0'=tmp99^post16, DName^0'=DName^post16, b22^0'=b22^post16, a11^0'=a11^post16, set^0'=set^post16, lptNamei^0'=lptNamei^post16, Pdoi^0'=Pdoi^post16, pc^0'=pc^post16, d44^0'=d44^post16, tmp55^0'=tmp55^post16, a88^0'=a88^post16, (d44^0-d44^post16 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post16 == 0 /\ status^0-status^post16 == 0 /\ i^0-i^post16 == 0 /\ -a88^post16+a88^0 == 0 /\ -i^0+Pdolen^0 <= 0 /\ -tmp55^post16+tmp55^0 == 0 /\ unset^0-unset^post16 == 0 /\ -Pdolen^post16+Pdolen^0 == 0 /\ PdoType^0-PdoType^post16 == 0 /\ -a11^post16+a11^0 == 0 /\ -dcIdi^post16+dcIdi^0 == 0 /\ -pc^post16+pc^0 == 0 /\ -tmp99^post16+tmp99^0 == 0 /\ -lptNamei^post16+lptNamei^0 == 0 /\ -b22^post16+b22^0 == 0 /\ c33^0-c33^post16 == 0 /\ -ret_PPMakeDeviceName66^post16+ret_PPMakeDeviceName66^0 == 0 /\ a1111^0-a1111^post16 == 0 /\ -set^post16+set^0 == 0 /\ -Pdoi^post16+Pdoi^0 == 0 /\ num^0-num^post16 == 0 /\ a77^0-a77^post16 == 0 /\ DName^0-DName^post16 == 0), cost: 1 11: l10 -> l7 : a1111^0'=a1111^post11, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post11, i^0'=i^post11, PdoType^0'=PdoType^post11, num^0'=num^post11, c33^0'=c33^post11, unset^0'=unset^post11, status^0'=status^post11, a77^0'=a77^post11, Pdolen^0'=Pdolen^post11, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post11, dcIdi^0'=dcIdi^post11, tmp99^0'=tmp99^post11, DName^0'=DName^post11, b22^0'=b22^post11, a11^0'=a11^post11, set^0'=set^post11, lptNamei^0'=lptNamei^post11, Pdoi^0'=Pdoi^post11, pc^0'=pc^post11, d44^0'=d44^post11, tmp55^0'=tmp55^post11, a88^0'=a88^post11, (0 == 0 /\ -tmp99^post11+ret_IoCreateDevice1010^post11 == 0 /\ a77^post11-DName^0 == 0 /\ -d44^post11+d44^0 == 0 /\ dcIdi^0-dcIdi^post11 == 0 /\ -unset^post11+unset^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post11 == 0 /\ a88^post11-Pdoi^0 == 0 /\ -Pdolen^post11+Pdolen^0 == 0 /\ -tmp55^post11+tmp55^0 == 0 /\ set^0-set^post11 == 0 /\ i^0-i^post11 == 0 /\ -lptNamei^post11+lptNamei^0 == 0 /\ b22^0-b22^post11 == 0 /\ DName^0 <= 0 /\ -DName^post11+DName^0 == 0 /\ -ret_IoCreateDevice1010^post11+status^post11 == 0 /\ c33^0-c33^post11 == 0 /\ num^0-num^post11 == 0 /\ -Pdoi^post11+Pdoi^0 == 0 /\ a11^0-a11^post11 == 0 /\ PdoType^0-PdoType^post11 == 0 /\ -1+pc^10 == 0 /\ pc^post11 == 0 /\ a1111^0-a1111^post11 == 0), cost: 1 12: l10 -> l2 : a1111^0'=a1111^post12, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post12, i^0'=i^post12, PdoType^0'=PdoType^post12, num^0'=num^post12, c33^0'=c33^post12, unset^0'=unset^post12, status^0'=status^post12, a77^0'=a77^post12, Pdolen^0'=Pdolen^post12, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post12, dcIdi^0'=dcIdi^post12, tmp99^0'=tmp99^post12, DName^0'=DName^post12, b22^0'=b22^post12, a11^0'=a11^post12, set^0'=set^post12, lptNamei^0'=lptNamei^post12, Pdoi^0'=Pdoi^post12, pc^0'=pc^post12, d44^0'=d44^post12, tmp55^0'=tmp55^post12, a88^0'=a88^post12, (status^0-status^post12 == 0 /\ -DName^post12+DName^0 == 0 /\ -a88^post12+a88^0 == 0 /\ Pdoi^0-Pdoi^post12 == 0 /\ dcIdi^0-dcIdi^post12 == 0 /\ i^0-i^post12 == 0 /\ -a77^post12+a77^0 == 0 /\ -tmp55^post12+tmp55^0 == 0 /\ -unset^post12+unset^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post12 == 0 /\ -ret_IoCreateDevice1010^post12+ret_IoCreateDevice1010^0 == 0 /\ -set^post12+set^0 == 0 /\ tmp99^0-tmp99^post12 == 0 /\ -d44^post12+d44^0 == 0 /\ b22^0-b22^post12 == 0 /\ c33^0-c33^post12 == 0 /\ a11^0-a11^post12 == 0 /\ -pc^post12+pc^0 == 0 /\ num^0-num^post12 == 0 /\ Pdolen^0-Pdolen^post12 == 0 /\ 1-DName^0 <= 0 /\ PdoType^0-PdoType^post12 == 0 /\ -lptNamei^post12+lptNamei^0 == 0 /\ a1111^0-a1111^post12 == 0), cost: 1 14: l11 -> l3 : a1111^0'=a1111^post14, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post14, i^0'=i^post14, PdoType^0'=PdoType^post14, num^0'=num^post14, c33^0'=c33^post14, unset^0'=unset^post14, status^0'=status^post14, a77^0'=a77^post14, Pdolen^0'=Pdolen^post14, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post14, dcIdi^0'=dcIdi^post14, tmp99^0'=tmp99^post14, DName^0'=DName^post14, b22^0'=b22^post14, a11^0'=a11^post14, set^0'=set^post14, lptNamei^0'=lptNamei^post14, Pdoi^0'=Pdoi^post14, pc^0'=pc^post14, d44^0'=d44^post14, tmp55^0'=tmp55^post14, a88^0'=a88^post14, (b22^0-b22^post14 == 0 /\ -a88^post14+a88^0 == 0 /\ -dcIdi^post14+dcIdi^0 == 0 /\ Pdoi^0-Pdoi^post14 == 0 /\ -a11^post14+a11^0 == 0 /\ -num^post14+num^0 == 0 /\ -d44^post14+d44^0 == 0 /\ i^0-i^post14 == 0 /\ -tmp55^post14+tmp55^0 == 0 /\ -tmp99^post14+tmp99^0 == 0 /\ -Pdolen^post14+Pdolen^0 == 0 /\ PdoType^0-PdoType^post14 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post14 == 0 /\ -set^post14+set^0 == 0 /\ a1111^0-a1111^post14 == 0 /\ -a77^post14+a77^0 == 0 /\ unset^0-unset^post14 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post14 == 0 /\ lptNamei^0-lptNamei^post14 == 0 /\ -DName^post14+DName^0 == 0 /\ -pc^post14+pc^0 == 0 /\ status^0-status^post14 == 0 /\ -c33^post14+c33^0 == 0), cost: 1 17: l12 -> l8 : a1111^0'=a1111^post17, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post17, i^0'=i^post17, PdoType^0'=PdoType^post17, num^0'=num^post17, c33^0'=c33^post17, unset^0'=unset^post17, status^0'=status^post17, a77^0'=a77^post17, Pdolen^0'=Pdolen^post17, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post17, dcIdi^0'=dcIdi^post17, tmp99^0'=tmp99^post17, DName^0'=DName^post17, b22^0'=b22^post17, a11^0'=a11^post17, set^0'=set^post17, lptNamei^0'=lptNamei^post17, Pdoi^0'=Pdoi^post17, pc^0'=pc^post17, d44^0'=d44^post17, tmp55^0'=tmp55^post17, a88^0'=a88^post17, (status^0-status^post17 == 0 /\ PdoType^0-PdoType^post17 == 0 /\ a77^0-a77^post17 == 0 /\ -tmp55^post17+tmp55^0 == 0 /\ -1+set^20 == 0 /\ i^0-i^post17 == 0 /\ -tmp99^post17+tmp99^0 == 0 /\ -Pdoi^post17+Pdoi^0 == 0 /\ unset^post17 == 0 /\ -b22^post17+b22^0 == 0 /\ a1111^0-a1111^post17 == 0 /\ -d44^post17+d44^0 == 0 /\ pc^0-pc^post17 == 0 /\ set^10-unset^post17 == 0 /\ num^0-num^post17 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post17 == 0 /\ -a11^post17+a11^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post17 == 0 /\ Pdolen^0-Pdolen^post17 == 0 /\ -dcIdi^post17+dcIdi^0 == 0 /\ DName^0-DName^post17 == 0 /\ -a88^post17+a88^0 == 0 /\ set^post17 == 0 /\ -lptNamei^post17+lptNamei^0 == 0 /\ -c33^post17+c33^0 == 0), cost: 1 18: l13 -> l12 : a1111^0'=a1111^post18, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post18, i^0'=i^post18, PdoType^0'=PdoType^post18, num^0'=num^post18, c33^0'=c33^post18, unset^0'=unset^post18, status^0'=status^post18, a77^0'=a77^post18, Pdolen^0'=Pdolen^post18, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post18, dcIdi^0'=dcIdi^post18, tmp99^0'=tmp99^post18, DName^0'=DName^post18, b22^0'=b22^post18, a11^0'=a11^post18, set^0'=set^post18, lptNamei^0'=lptNamei^post18, Pdoi^0'=Pdoi^post18, pc^0'=pc^post18, d44^0'=d44^post18, tmp55^0'=tmp55^post18, a88^0'=a88^post18, (-PdoType^post18+PdoType^0 == 0 /\ -status^post18+status^0 == 0 /\ -set^post18+set^0 == 0 /\ unset^0-unset^post18 == 0 /\ -a11^post18+a11^0 == 0 /\ -pc^post18+pc^0 == 0 /\ num^0-num^post18 == 0 /\ c33^0-c33^post18 == 0 /\ i^0-i^post18 == 0 /\ a1111^0-a1111^post18 == 0 /\ DName^0-DName^post18 == 0 /\ Pdolen^0-Pdolen^post18 == 0 /\ -b22^post18+b22^0 == 0 /\ a77^0-a77^post18 == 0 /\ -lptNamei^post18+lptNamei^0 == 0 /\ -d44^post18+d44^0 == 0 /\ tmp99^0-tmp99^post18 == 0 /\ -tmp55^post18+tmp55^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post18 == 0 /\ -Pdoi^post18+Pdoi^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post18 == 0 /\ -dcIdi^post18+dcIdi^0 == 0 /\ -a88^post18+a88^0 == 0), cost: 1 Removed unreachable rules and leafs Start location: l13 1: l2 -> l3 : a1111^0'=a1111^post1, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post1, i^0'=i^post1, PdoType^0'=PdoType^post1, num^0'=num^post1, c33^0'=c33^post1, unset^0'=unset^post1, status^0'=status^post1, a77^0'=a77^post1, Pdolen^0'=Pdolen^post1, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post1, dcIdi^0'=dcIdi^post1, tmp99^0'=tmp99^post1, DName^0'=DName^post1, b22^0'=b22^post1, a11^0'=a11^post1, set^0'=set^post1, lptNamei^0'=lptNamei^post1, Pdoi^0'=Pdoi^post1, pc^0'=pc^post1, d44^0'=d44^post1, tmp55^0'=tmp55^post1, a88^0'=a88^post1, (unset^post1 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post1 == 0 /\ tmp99^0-tmp99^post1 == 0 /\ -1+unset^10 == 0 /\ -lptNamei^post1+lptNamei^0 == 0 /\ dcIdi^0-dcIdi^post1 == 0 /\ -pc^post1+pc^0 == 0 /\ a1111^0-a1111^post1 == 0 /\ -ret_IoCreateDevice1010^post1+ret_IoCreateDevice1010^0 == 0 /\ PdoType^0-PdoType^post1 == 0 /\ Pdolen^0-Pdolen^post1 == 0 /\ -Pdoi^post1+Pdoi^0 == 0 /\ set^0-set^post1 == 0 /\ -status^post1+status^0 == 0 /\ -tmp55^post1+tmp55^0 == 0 /\ num^post1 == 0 /\ -a88^post1+a88^0 == 0 /\ a11^0-a11^post1 == 0 /\ -DName^post1+DName^0 == 0 /\ -b22^post1+b22^0 == 0 /\ -i^post1+i^0 == 0 /\ a77^0-a77^post1 == 0 /\ c33^0-c33^post1 == 0 /\ -d44^post1+d44^0 == 0), cost: 1 13: l3 -> l11 : a1111^0'=a1111^post13, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post13, i^0'=i^post13, PdoType^0'=PdoType^post13, num^0'=num^post13, c33^0'=c33^post13, unset^0'=unset^post13, status^0'=status^post13, a77^0'=a77^post13, Pdolen^0'=Pdolen^post13, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post13, dcIdi^0'=dcIdi^post13, tmp99^0'=tmp99^post13, DName^0'=DName^post13, b22^0'=b22^post13, a11^0'=a11^post13, set^0'=set^post13, lptNamei^0'=lptNamei^post13, Pdoi^0'=Pdoi^post13, pc^0'=pc^post13, d44^0'=d44^post13, tmp55^0'=tmp55^post13, a88^0'=a88^post13, (-a77^post13+a77^0 == 0 /\ -d44^post13+d44^0 == 0 /\ -a88^post13+a88^0 == 0 /\ Pdoi^0-Pdoi^post13 == 0 /\ i^0-i^post13 == 0 /\ -tmp55^post13+tmp55^0 == 0 /\ unset^0-unset^post13 == 0 /\ -Pdolen^post13+Pdolen^0 == 0 /\ -lptNamei^post13+lptNamei^0 == 0 /\ a1111^0-a1111^post13 == 0 /\ -set^post13+set^0 == 0 /\ b22^0-b22^post13 == 0 /\ PdoType^0-PdoType^post13 == 0 /\ dcIdi^0-dcIdi^post13 == 0 /\ status^0-status^post13 == 0 /\ -ret_IoCreateDevice1010^post13+ret_IoCreateDevice1010^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post13 == 0 /\ -num^post13+num^0 == 0 /\ -pc^post13+pc^0 == 0 /\ a11^0-a11^post13 == 0 /\ -c33^post13+c33^0 == 0 /\ -tmp99^post13+tmp99^0 == 0 /\ -DName^post13+DName^0 == 0), cost: 1 2: l4 -> l2 : a1111^0'=a1111^post2, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post2, i^0'=i^post2, PdoType^0'=PdoType^post2, num^0'=num^post2, c33^0'=c33^post2, unset^0'=unset^post2, status^0'=status^post2, a77^0'=a77^post2, Pdolen^0'=Pdolen^post2, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post2, dcIdi^0'=dcIdi^post2, tmp99^0'=tmp99^post2, DName^0'=DName^post2, b22^0'=b22^post2, a11^0'=a11^post2, set^0'=set^post2, lptNamei^0'=lptNamei^post2, Pdoi^0'=Pdoi^post2, pc^0'=pc^post2, d44^0'=d44^post2, tmp55^0'=tmp55^post2, a88^0'=a88^post2, (-set^post2+set^0 == 0 /\ -DName^post2+DName^0 == 0 /\ PdoType^0-PdoType^post2 == 0 /\ a1111^0-a1111^post2 == 0 /\ -ret_IoCreateDevice1010^post2+ret_IoCreateDevice1010^0 == 0 /\ -pc^post2+pc^0 == 0 /\ -Pdoi^post2+Pdoi^0 == 0 /\ status^0-status^post2 == 0 /\ i^0-i^post2 == 0 /\ tmp99^0-tmp99^post2 == 0 /\ -d44^post2+d44^0 == 0 /\ num^0-num^post2 == 0 /\ c33^0-c33^post2 == 0 /\ -a77^post2+a77^0 == 0 /\ b22^0-b22^post2 == 0 /\ -tmp55^post2+tmp55^0 == 0 /\ -unset^post2+unset^0 == 0 /\ a11^0-a11^post2 == 0 /\ dcIdi^0-dcIdi^post2 == 0 /\ Pdolen^0-Pdolen^post2 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post2 == 0 /\ -lptNamei^post2+lptNamei^0 == 0 /\ -a88^post2+a88^0 == 0), cost: 1 3: l5 -> l4 : a1111^0'=a1111^post3, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post3, i^0'=i^post3, PdoType^0'=PdoType^post3, num^0'=num^post3, c33^0'=c33^post3, unset^0'=unset^post3, status^0'=status^post3, a77^0'=a77^post3, Pdolen^0'=Pdolen^post3, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post3, dcIdi^0'=dcIdi^post3, tmp99^0'=tmp99^post3, DName^0'=DName^post3, b22^0'=b22^post3, a11^0'=a11^post3, set^0'=set^post3, lptNamei^0'=lptNamei^post3, Pdoi^0'=Pdoi^post3, pc^0'=pc^post3, d44^0'=d44^post3, tmp55^0'=tmp55^post3, a88^0'=a88^post3, (-a77^post3+a77^0 == 0 /\ -set^post3+set^0 == 0 /\ a1111^0-a1111^post3 == 0 /\ b22^0-b22^post3 == 0 /\ unset^0-unset^post3 == 0 /\ -pc^post3+pc^0 == 0 /\ -1+status^0 <= 0 /\ i^0-i^post3 == 0 /\ -DName^post3+DName^0 == 0 /\ PdoType^0-PdoType^post3 == 0 /\ dcIdi^0-dcIdi^post3 == 0 /\ status^0-status^post3 == 0 /\ -d44^post3+d44^0 == 0 /\ c33^0-c33^post3 == 0 /\ -a11^post3+a11^0 == 0 /\ -tmp55^post3+tmp55^0 == 0 /\ -tmp99^post3+tmp99^0 == 0 /\ -Pdolen^post3+Pdolen^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post3 == 0 /\ -Pdoi^post3+Pdoi^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post3 == 0 /\ -num^post3+num^0 == 0 /\ lptNamei^0-lptNamei^post3 == 0 /\ -a88^post3+a88^0 == 0), cost: 1 4: l5 -> l4 : a1111^0'=a1111^post4, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post4, i^0'=i^post4, PdoType^0'=PdoType^post4, num^0'=num^post4, c33^0'=c33^post4, unset^0'=unset^post4, status^0'=status^post4, a77^0'=a77^post4, Pdolen^0'=Pdolen^post4, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post4, dcIdi^0'=dcIdi^post4, tmp99^0'=tmp99^post4, DName^0'=DName^post4, b22^0'=b22^post4, a11^0'=a11^post4, set^0'=set^post4, lptNamei^0'=lptNamei^post4, Pdoi^0'=Pdoi^post4, pc^0'=pc^post4, d44^0'=d44^post4, tmp55^0'=tmp55^post4, a88^0'=a88^post4, (-a77^post4+a77^0 == 0 /\ -a88^post4+a88^0 == 0 /\ -a11^post4+a11^0 == 0 /\ Pdoi^0-Pdoi^post4 == 0 /\ -d44^post4+d44^0 == 0 /\ i^0-i^post4 == 0 /\ -tmp55^post4+tmp55^0 == 0 /\ unset^0-unset^post4 == 0 /\ -tmp99^post4+tmp99^0 == 0 /\ 3-status^0 <= 0 /\ b22^0-b22^post4 == 0 /\ a1111^0-a1111^post4 == 0 /\ PdoType^0-PdoType^post4 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post4 == 0 /\ lptNamei^0-lptNamei^post4 == 0 /\ dcIdi^0-dcIdi^post4 == 0 /\ status^0-status^post4 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post4 == 0 /\ -Pdolen^post4+Pdolen^0 == 0 /\ -num^post4+num^0 == 0 /\ -DName^post4+DName^0 == 0 /\ -pc^post4+pc^0 == 0 /\ -c33^post4+c33^0 == 0 /\ -set^post4+set^0 == 0), cost: 1 5: l5 -> l4 : a1111^0'=a1111^post5, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post5, i^0'=i^post5, PdoType^0'=PdoType^post5, num^0'=num^post5, c33^0'=c33^post5, unset^0'=unset^post5, status^0'=status^post5, a77^0'=a77^post5, Pdolen^0'=Pdolen^post5, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post5, dcIdi^0'=dcIdi^post5, tmp99^0'=tmp99^post5, DName^0'=DName^post5, b22^0'=b22^post5, a11^0'=a11^post5, set^0'=set^post5, lptNamei^0'=lptNamei^post5, Pdoi^0'=Pdoi^post5, pc^0'=pc^post5, d44^0'=d44^post5, tmp55^0'=tmp55^post5, a88^0'=a88^post5, (-dcIdi^post5+dcIdi^0 == 0 /\ b22^0-b22^post5 == 0 /\ -tmp99^post5+tmp99^0 == 0 /\ -tmp55^post5+tmp55^0 == 0 /\ 2-status^0 <= 0 /\ -Pdoi^post5+Pdoi^0 == 0 /\ -a11^post5+a11^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post5 == 0 /\ -d44^post5+d44^0 == 0 /\ -Pdolen^post5+Pdolen^0 == 0 /\ -a88^post5+a88^0 == 0 /\ -set^post5+set^0 == 0 /\ unset^0-unset^post5 == 0 /\ PdoType^0-PdoType^post5 == 0 /\ -a77^post5+a77^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post5 == 0 /\ lptNamei^0-lptNamei^post5 == 0 /\ -2+status^0 <= 0 /\ -1-num^0+num^post5 == 0 /\ i^0-i^post5 == 0 /\ -DName^post5+DName^0 == 0 /\ -DName^0+a1111^post5 == 0 /\ -pc^post5+pc^0 == 0 /\ status^0-status^post5 == 0 /\ c33^0-c33^post5 == 0), cost: 1 6: l6 -> l5 : a1111^0'=a1111^post6, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post6, i^0'=i^post6, PdoType^0'=PdoType^post6, num^0'=num^post6, c33^0'=c33^post6, unset^0'=unset^post6, status^0'=status^post6, a77^0'=a77^post6, Pdolen^0'=Pdolen^post6, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post6, dcIdi^0'=dcIdi^post6, tmp99^0'=tmp99^post6, DName^0'=DName^post6, b22^0'=b22^post6, a11^0'=a11^post6, set^0'=set^post6, lptNamei^0'=lptNamei^post6, Pdoi^0'=Pdoi^post6, pc^0'=pc^post6, d44^0'=d44^post6, tmp55^0'=tmp55^post6, a88^0'=a88^post6, (Pdoi^post6 == 0 /\ Pdolen^0-Pdolen^post6 == 0 /\ -dcIdi^post6+dcIdi^0 == 0 /\ -lptNamei^post6+lptNamei^0 == 0 /\ a77^0-a77^post6 == 0 /\ -a88^post6+a88^0 == 0 /\ -b22^post6+b22^0 == 0 /\ i^0-i^post6 == 0 /\ -d44^post6+d44^0 == 0 /\ -set^post6+set^0 == 0 /\ -tmp99^post6+tmp99^0 == 0 /\ status^0-status^post6 == 0 /\ -tmp55^post6+tmp55^0 == 0 /\ -pc^post6+pc^0 == 0 /\ c33^0-c33^post6 == 0 /\ -ret_PPMakeDeviceName66^post6+ret_PPMakeDeviceName66^0 == 0 /\ DName^0-DName^post6 == 0 /\ a1111^0-a1111^post6 == 0 /\ unset^0-unset^post6 == 0 /\ PdoType^0-PdoType^post6 == 0 /\ -a11^post6+a11^0 == 0 /\ num^0-num^post6 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post6 == 0), cost: 1 7: l7 -> l8 : a1111^0'=a1111^post7, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post7, i^0'=i^post7, PdoType^0'=PdoType^post7, num^0'=num^post7, c33^0'=c33^post7, unset^0'=unset^post7, status^0'=status^post7, a77^0'=a77^post7, Pdolen^0'=Pdolen^post7, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post7, dcIdi^0'=dcIdi^post7, tmp99^0'=tmp99^post7, DName^0'=DName^post7, b22^0'=b22^post7, a11^0'=a11^post7, set^0'=set^post7, lptNamei^0'=lptNamei^post7, Pdoi^0'=Pdoi^post7, pc^0'=pc^post7, d44^0'=d44^post7, tmp55^0'=tmp55^post7, a88^0'=a88^post7, (-ret_IoCreateDevice1010^post7+ret_IoCreateDevice1010^0 == 0 /\ -pc^post7+pc^0 == 0 /\ a1111^0-a1111^post7 == 0 /\ unset^0-unset^post7 == 0 /\ -set^post7+set^0 == 0 /\ -status^post7+status^0 == 0 /\ Pdolen^0-Pdolen^post7 == 0 /\ DName^0-DName^post7 == 0 /\ -b22^post7+b22^0 == 0 /\ c33^0-c33^post7 == 0 /\ 1-status^0 <= 0 /\ -1+status^0 <= 0 /\ -d44^post7+d44^0 == 0 /\ -Pdoi^post7+Pdoi^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post7 == 0 /\ -1-i^0+i^post7 == 0 /\ a77^0-a77^post7 == 0 /\ dcIdi^0-dcIdi^post7 == 0 /\ num^0-num^post7 == 0 /\ -a11^post7+a11^0 == 0 /\ -tmp55^post7+tmp55^0 == 0 /\ -PdoType^post7+PdoType^0 == 0 /\ -a88^post7+a88^0 == 0 /\ tmp99^0-tmp99^post7 == 0 /\ -lptNamei^post7+lptNamei^0 == 0), cost: 1 8: l7 -> l6 : a1111^0'=a1111^post8, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post8, i^0'=i^post8, PdoType^0'=PdoType^post8, num^0'=num^post8, c33^0'=c33^post8, unset^0'=unset^post8, status^0'=status^post8, a77^0'=a77^post8, Pdolen^0'=Pdolen^post8, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post8, dcIdi^0'=dcIdi^post8, tmp99^0'=tmp99^post8, DName^0'=DName^post8, b22^0'=b22^post8, a11^0'=a11^post8, set^0'=set^post8, lptNamei^0'=lptNamei^post8, Pdoi^0'=Pdoi^post8, pc^0'=pc^post8, d44^0'=d44^post8, tmp55^0'=tmp55^post8, a88^0'=a88^post8, (c33^0-c33^post8 == 0 /\ -PdoType^post8+PdoType^0 == 0 /\ -pc^post8+pc^0 == 0 /\ unset^0-unset^post8 == 0 /\ -status^post8+status^0 == 0 /\ -ret_IoCreateDevice1010^post8+ret_IoCreateDevice1010^0 == 0 /\ num^0-num^post8 == 0 /\ a11^0-a11^post8 == 0 /\ a1111^0-a1111^post8 == 0 /\ status^0 <= 0 /\ DName^0-DName^post8 == 0 /\ Pdolen^0-Pdolen^post8 == 0 /\ -tmp55^post8+tmp55^0 == 0 /\ -Pdoi^post8+Pdoi^0 == 0 /\ -b22^post8+b22^0 == 0 /\ a77^0-a77^post8 == 0 /\ dcIdi^0-dcIdi^post8 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post8 == 0 /\ i^0-i^post8 == 0 /\ tmp99^0-tmp99^post8 == 0 /\ -a88^post8+a88^0 == 0 /\ -lptNamei^post8+lptNamei^0 == 0 /\ -d44^post8+d44^0 == 0 /\ set^0-set^post8 == 0), cost: 1 9: l7 -> l6 : a1111^0'=a1111^post9, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post9, i^0'=i^post9, PdoType^0'=PdoType^post9, num^0'=num^post9, c33^0'=c33^post9, unset^0'=unset^post9, status^0'=status^post9, a77^0'=a77^post9, Pdolen^0'=Pdolen^post9, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post9, dcIdi^0'=dcIdi^post9, tmp99^0'=tmp99^post9, DName^0'=DName^post9, b22^0'=b22^post9, a11^0'=a11^post9, set^0'=set^post9, lptNamei^0'=lptNamei^post9, Pdoi^0'=Pdoi^post9, pc^0'=pc^post9, d44^0'=d44^post9, tmp55^0'=tmp55^post9, a88^0'=a88^post9, (pc^0-pc^post9 == 0 /\ dcIdi^0-dcIdi^post9 == 0 /\ -d44^post9+d44^0 == 0 /\ -a88^post9+a88^0 == 0 /\ -a77^post9+a77^0 == 0 /\ 2-status^0 <= 0 /\ -unset^post9+unset^0 == 0 /\ -Pdoi^post9+Pdoi^0 == 0 /\ tmp99^0-tmp99^post9 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post9 == 0 /\ -tmp55^post9+tmp55^0 == 0 /\ a11^0-a11^post9 == 0 /\ -lptNamei^post9+lptNamei^0 == 0 /\ Pdolen^0-Pdolen^post9 == 0 /\ -status^post9+status^0 == 0 /\ -DName^post9+DName^0 == 0 /\ i^0-i^post9 == 0 /\ -ret_IoCreateDevice1010^post9+ret_IoCreateDevice1010^0 == 0 /\ set^0-set^post9 == 0 /\ num^0-num^post9 == 0 /\ c33^0-c33^post9 == 0 /\ -b22^post9+b22^0 == 0 /\ a1111^0-a1111^post9 == 0 /\ PdoType^0-PdoType^post9 == 0), cost: 1 10: l8 -> l9 : a1111^0'=a1111^post10, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post10, i^0'=i^post10, PdoType^0'=PdoType^post10, num^0'=num^post10, c33^0'=c33^post10, unset^0'=unset^post10, status^0'=status^post10, a77^0'=a77^post10, Pdolen^0'=Pdolen^post10, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post10, dcIdi^0'=dcIdi^post10, tmp99^0'=tmp99^post10, DName^0'=DName^post10, b22^0'=b22^post10, a11^0'=a11^post10, set^0'=set^post10, lptNamei^0'=lptNamei^post10, Pdoi^0'=Pdoi^post10, pc^0'=pc^post10, d44^0'=d44^post10, tmp55^0'=tmp55^post10, a88^0'=a88^post10, (pc^0-pc^post10 == 0 /\ -lptNamei^post10+lptNamei^0 == 0 /\ -a88^post10+a88^0 == 0 /\ a1111^0-a1111^post10 == 0 /\ -d44^post10+d44^0 == 0 /\ PdoType^0-PdoType^post10 == 0 /\ -tmp55^post10+tmp55^0 == 0 /\ -Pdolen^post10+Pdolen^0 == 0 /\ -Pdoi^post10+Pdoi^0 == 0 /\ -ret_IoCreateDevice1010^post10+ret_IoCreateDevice1010^0 == 0 /\ tmp99^0-tmp99^post10 == 0 /\ status^0-status^post10 == 0 /\ -a77^post10+a77^0 == 0 /\ b22^0-b22^post10 == 0 /\ -unset^post10+unset^0 == 0 /\ num^0-num^post10 == 0 /\ i^0-i^post10 == 0 /\ set^0-set^post10 == 0 /\ a11^0-a11^post10 == 0 /\ c33^0-c33^post10 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post10 == 0 /\ -DName^post10+DName^0 == 0 /\ dcIdi^0-dcIdi^post10 == 0), cost: 1 15: l9 -> l10 : a1111^0'=a1111^post15, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post15, i^0'=i^post15, PdoType^0'=PdoType^post15, num^0'=num^post15, c33^0'=c33^post15, unset^0'=unset^post15, status^0'=status^post15, a77^0'=a77^post15, Pdolen^0'=Pdolen^post15, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post15, dcIdi^0'=dcIdi^post15, tmp99^0'=tmp99^post15, DName^0'=DName^post15, b22^0'=b22^post15, a11^0'=a11^post15, set^0'=set^post15, lptNamei^0'=lptNamei^post15, Pdoi^0'=Pdoi^post15, pc^0'=pc^post15, d44^0'=d44^post15, tmp55^0'=tmp55^post15, a88^0'=a88^post15, (0 == 0 /\ -dcIdi^post15+dcIdi^0 == 0 /\ ret_PPMakeDeviceName66^post15-tmp55^post15 == 0 /\ 1+i^0-Pdolen^0 <= 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post15 == 0 /\ -num^post15+num^0 == 0 /\ -Pdolen^post15+Pdolen^0 == 0 /\ Pdoi^0-Pdoi^post15 == 0 /\ -set^post15+set^0 == 0 /\ unset^0-unset^post15 == 0 /\ PdoType^0-PdoType^post15 == 0 /\ -a77^post15+a77^0 == 0 /\ -pc^post15+pc^0 == 0 /\ -tmp99^post15+tmp99^0 == 0 /\ -PdoType^0+b22^post15 == 0 /\ a1111^0-a1111^post15 == 0 /\ -a88^post15+a88^0 == 0 /\ DName^post15-ret_PPMakeDeviceName66^post15 == 0 /\ c33^post15-dcIdi^0 == 0 /\ -lptNamei^post15+lptNamei^0 == 0 /\ status^0-status^post15 == 0 /\ a11^post15-lptNamei^0 == 0 /\ i^0-i^post15 == 0 /\ -num^0+d44^post15 == 0), cost: 1 16: l9 -> l2 : a1111^0'=a1111^post16, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post16, i^0'=i^post16, PdoType^0'=PdoType^post16, num^0'=num^post16, c33^0'=c33^post16, unset^0'=unset^post16, status^0'=status^post16, a77^0'=a77^post16, Pdolen^0'=Pdolen^post16, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post16, dcIdi^0'=dcIdi^post16, tmp99^0'=tmp99^post16, DName^0'=DName^post16, b22^0'=b22^post16, a11^0'=a11^post16, set^0'=set^post16, lptNamei^0'=lptNamei^post16, Pdoi^0'=Pdoi^post16, pc^0'=pc^post16, d44^0'=d44^post16, tmp55^0'=tmp55^post16, a88^0'=a88^post16, (d44^0-d44^post16 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post16 == 0 /\ status^0-status^post16 == 0 /\ i^0-i^post16 == 0 /\ -a88^post16+a88^0 == 0 /\ -i^0+Pdolen^0 <= 0 /\ -tmp55^post16+tmp55^0 == 0 /\ unset^0-unset^post16 == 0 /\ -Pdolen^post16+Pdolen^0 == 0 /\ PdoType^0-PdoType^post16 == 0 /\ -a11^post16+a11^0 == 0 /\ -dcIdi^post16+dcIdi^0 == 0 /\ -pc^post16+pc^0 == 0 /\ -tmp99^post16+tmp99^0 == 0 /\ -lptNamei^post16+lptNamei^0 == 0 /\ -b22^post16+b22^0 == 0 /\ c33^0-c33^post16 == 0 /\ -ret_PPMakeDeviceName66^post16+ret_PPMakeDeviceName66^0 == 0 /\ a1111^0-a1111^post16 == 0 /\ -set^post16+set^0 == 0 /\ -Pdoi^post16+Pdoi^0 == 0 /\ num^0-num^post16 == 0 /\ a77^0-a77^post16 == 0 /\ DName^0-DName^post16 == 0), cost: 1 11: l10 -> l7 : a1111^0'=a1111^post11, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post11, i^0'=i^post11, PdoType^0'=PdoType^post11, num^0'=num^post11, c33^0'=c33^post11, unset^0'=unset^post11, status^0'=status^post11, a77^0'=a77^post11, Pdolen^0'=Pdolen^post11, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post11, dcIdi^0'=dcIdi^post11, tmp99^0'=tmp99^post11, DName^0'=DName^post11, b22^0'=b22^post11, a11^0'=a11^post11, set^0'=set^post11, lptNamei^0'=lptNamei^post11, Pdoi^0'=Pdoi^post11, pc^0'=pc^post11, d44^0'=d44^post11, tmp55^0'=tmp55^post11, a88^0'=a88^post11, (0 == 0 /\ -tmp99^post11+ret_IoCreateDevice1010^post11 == 0 /\ a77^post11-DName^0 == 0 /\ -d44^post11+d44^0 == 0 /\ dcIdi^0-dcIdi^post11 == 0 /\ -unset^post11+unset^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post11 == 0 /\ a88^post11-Pdoi^0 == 0 /\ -Pdolen^post11+Pdolen^0 == 0 /\ -tmp55^post11+tmp55^0 == 0 /\ set^0-set^post11 == 0 /\ i^0-i^post11 == 0 /\ -lptNamei^post11+lptNamei^0 == 0 /\ b22^0-b22^post11 == 0 /\ DName^0 <= 0 /\ -DName^post11+DName^0 == 0 /\ -ret_IoCreateDevice1010^post11+status^post11 == 0 /\ c33^0-c33^post11 == 0 /\ num^0-num^post11 == 0 /\ -Pdoi^post11+Pdoi^0 == 0 /\ a11^0-a11^post11 == 0 /\ PdoType^0-PdoType^post11 == 0 /\ -1+pc^10 == 0 /\ pc^post11 == 0 /\ a1111^0-a1111^post11 == 0), cost: 1 12: l10 -> l2 : a1111^0'=a1111^post12, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post12, i^0'=i^post12, PdoType^0'=PdoType^post12, num^0'=num^post12, c33^0'=c33^post12, unset^0'=unset^post12, status^0'=status^post12, a77^0'=a77^post12, Pdolen^0'=Pdolen^post12, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post12, dcIdi^0'=dcIdi^post12, tmp99^0'=tmp99^post12, DName^0'=DName^post12, b22^0'=b22^post12, a11^0'=a11^post12, set^0'=set^post12, lptNamei^0'=lptNamei^post12, Pdoi^0'=Pdoi^post12, pc^0'=pc^post12, d44^0'=d44^post12, tmp55^0'=tmp55^post12, a88^0'=a88^post12, (status^0-status^post12 == 0 /\ -DName^post12+DName^0 == 0 /\ -a88^post12+a88^0 == 0 /\ Pdoi^0-Pdoi^post12 == 0 /\ dcIdi^0-dcIdi^post12 == 0 /\ i^0-i^post12 == 0 /\ -a77^post12+a77^0 == 0 /\ -tmp55^post12+tmp55^0 == 0 /\ -unset^post12+unset^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post12 == 0 /\ -ret_IoCreateDevice1010^post12+ret_IoCreateDevice1010^0 == 0 /\ -set^post12+set^0 == 0 /\ tmp99^0-tmp99^post12 == 0 /\ -d44^post12+d44^0 == 0 /\ b22^0-b22^post12 == 0 /\ c33^0-c33^post12 == 0 /\ a11^0-a11^post12 == 0 /\ -pc^post12+pc^0 == 0 /\ num^0-num^post12 == 0 /\ Pdolen^0-Pdolen^post12 == 0 /\ 1-DName^0 <= 0 /\ PdoType^0-PdoType^post12 == 0 /\ -lptNamei^post12+lptNamei^0 == 0 /\ a1111^0-a1111^post12 == 0), cost: 1 14: l11 -> l3 : a1111^0'=a1111^post14, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post14, i^0'=i^post14, PdoType^0'=PdoType^post14, num^0'=num^post14, c33^0'=c33^post14, unset^0'=unset^post14, status^0'=status^post14, a77^0'=a77^post14, Pdolen^0'=Pdolen^post14, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post14, dcIdi^0'=dcIdi^post14, tmp99^0'=tmp99^post14, DName^0'=DName^post14, b22^0'=b22^post14, a11^0'=a11^post14, set^0'=set^post14, lptNamei^0'=lptNamei^post14, Pdoi^0'=Pdoi^post14, pc^0'=pc^post14, d44^0'=d44^post14, tmp55^0'=tmp55^post14, a88^0'=a88^post14, (b22^0-b22^post14 == 0 /\ -a88^post14+a88^0 == 0 /\ -dcIdi^post14+dcIdi^0 == 0 /\ Pdoi^0-Pdoi^post14 == 0 /\ -a11^post14+a11^0 == 0 /\ -num^post14+num^0 == 0 /\ -d44^post14+d44^0 == 0 /\ i^0-i^post14 == 0 /\ -tmp55^post14+tmp55^0 == 0 /\ -tmp99^post14+tmp99^0 == 0 /\ -Pdolen^post14+Pdolen^0 == 0 /\ PdoType^0-PdoType^post14 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post14 == 0 /\ -set^post14+set^0 == 0 /\ a1111^0-a1111^post14 == 0 /\ -a77^post14+a77^0 == 0 /\ unset^0-unset^post14 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post14 == 0 /\ lptNamei^0-lptNamei^post14 == 0 /\ -DName^post14+DName^0 == 0 /\ -pc^post14+pc^0 == 0 /\ status^0-status^post14 == 0 /\ -c33^post14+c33^0 == 0), cost: 1 17: l12 -> l8 : a1111^0'=a1111^post17, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post17, i^0'=i^post17, PdoType^0'=PdoType^post17, num^0'=num^post17, c33^0'=c33^post17, unset^0'=unset^post17, status^0'=status^post17, a77^0'=a77^post17, Pdolen^0'=Pdolen^post17, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post17, dcIdi^0'=dcIdi^post17, tmp99^0'=tmp99^post17, DName^0'=DName^post17, b22^0'=b22^post17, a11^0'=a11^post17, set^0'=set^post17, lptNamei^0'=lptNamei^post17, Pdoi^0'=Pdoi^post17, pc^0'=pc^post17, d44^0'=d44^post17, tmp55^0'=tmp55^post17, a88^0'=a88^post17, (status^0-status^post17 == 0 /\ PdoType^0-PdoType^post17 == 0 /\ a77^0-a77^post17 == 0 /\ -tmp55^post17+tmp55^0 == 0 /\ -1+set^20 == 0 /\ i^0-i^post17 == 0 /\ -tmp99^post17+tmp99^0 == 0 /\ -Pdoi^post17+Pdoi^0 == 0 /\ unset^post17 == 0 /\ -b22^post17+b22^0 == 0 /\ a1111^0-a1111^post17 == 0 /\ -d44^post17+d44^0 == 0 /\ pc^0-pc^post17 == 0 /\ set^10-unset^post17 == 0 /\ num^0-num^post17 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post17 == 0 /\ -a11^post17+a11^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post17 == 0 /\ Pdolen^0-Pdolen^post17 == 0 /\ -dcIdi^post17+dcIdi^0 == 0 /\ DName^0-DName^post17 == 0 /\ -a88^post17+a88^0 == 0 /\ set^post17 == 0 /\ -lptNamei^post17+lptNamei^0 == 0 /\ -c33^post17+c33^0 == 0), cost: 1 18: l13 -> l12 : a1111^0'=a1111^post18, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post18, i^0'=i^post18, PdoType^0'=PdoType^post18, num^0'=num^post18, c33^0'=c33^post18, unset^0'=unset^post18, status^0'=status^post18, a77^0'=a77^post18, Pdolen^0'=Pdolen^post18, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post18, dcIdi^0'=dcIdi^post18, tmp99^0'=tmp99^post18, DName^0'=DName^post18, b22^0'=b22^post18, a11^0'=a11^post18, set^0'=set^post18, lptNamei^0'=lptNamei^post18, Pdoi^0'=Pdoi^post18, pc^0'=pc^post18, d44^0'=d44^post18, tmp55^0'=tmp55^post18, a88^0'=a88^post18, (-PdoType^post18+PdoType^0 == 0 /\ -status^post18+status^0 == 0 /\ -set^post18+set^0 == 0 /\ unset^0-unset^post18 == 0 /\ -a11^post18+a11^0 == 0 /\ -pc^post18+pc^0 == 0 /\ num^0-num^post18 == 0 /\ c33^0-c33^post18 == 0 /\ i^0-i^post18 == 0 /\ a1111^0-a1111^post18 == 0 /\ DName^0-DName^post18 == 0 /\ Pdolen^0-Pdolen^post18 == 0 /\ -b22^post18+b22^0 == 0 /\ a77^0-a77^post18 == 0 /\ -lptNamei^post18+lptNamei^0 == 0 /\ -d44^post18+d44^0 == 0 /\ tmp99^0-tmp99^post18 == 0 /\ -tmp55^post18+tmp55^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post18 == 0 /\ -Pdoi^post18+Pdoi^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post18 == 0 /\ -dcIdi^post18+dcIdi^0 == 0 /\ -a88^post18+a88^0 == 0), cost: 1 Applied preprocessing Original rule: l2 -> l3 : a1111^0'=a1111^post1, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post1, i^0'=i^post1, PdoType^0'=PdoType^post1, num^0'=num^post1, c33^0'=c33^post1, unset^0'=unset^post1, status^0'=status^post1, a77^0'=a77^post1, Pdolen^0'=Pdolen^post1, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post1, dcIdi^0'=dcIdi^post1, tmp99^0'=tmp99^post1, DName^0'=DName^post1, b22^0'=b22^post1, a11^0'=a11^post1, set^0'=set^post1, lptNamei^0'=lptNamei^post1, Pdoi^0'=Pdoi^post1, pc^0'=pc^post1, d44^0'=d44^post1, tmp55^0'=tmp55^post1, a88^0'=a88^post1, (unset^post1 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post1 == 0 /\ tmp99^0-tmp99^post1 == 0 /\ -1+unset^10 == 0 /\ -lptNamei^post1+lptNamei^0 == 0 /\ dcIdi^0-dcIdi^post1 == 0 /\ -pc^post1+pc^0 == 0 /\ a1111^0-a1111^post1 == 0 /\ -ret_IoCreateDevice1010^post1+ret_IoCreateDevice1010^0 == 0 /\ PdoType^0-PdoType^post1 == 0 /\ Pdolen^0-Pdolen^post1 == 0 /\ -Pdoi^post1+Pdoi^0 == 0 /\ set^0-set^post1 == 0 /\ -status^post1+status^0 == 0 /\ -tmp55^post1+tmp55^0 == 0 /\ num^post1 == 0 /\ -a88^post1+a88^0 == 0 /\ a11^0-a11^post1 == 0 /\ -DName^post1+DName^0 == 0 /\ -b22^post1+b22^0 == 0 /\ -i^post1+i^0 == 0 /\ a77^0-a77^post1 == 0 /\ c33^0-c33^post1 == 0 /\ -d44^post1+d44^0 == 0), cost: 1 New rule: l2 -> l3 : num^0'=0, unset^0'=0, TRUE, cost: 1 Applied preprocessing Original rule: l4 -> l2 : a1111^0'=a1111^post2, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post2, i^0'=i^post2, PdoType^0'=PdoType^post2, num^0'=num^post2, c33^0'=c33^post2, unset^0'=unset^post2, status^0'=status^post2, a77^0'=a77^post2, Pdolen^0'=Pdolen^post2, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post2, dcIdi^0'=dcIdi^post2, tmp99^0'=tmp99^post2, DName^0'=DName^post2, b22^0'=b22^post2, a11^0'=a11^post2, set^0'=set^post2, lptNamei^0'=lptNamei^post2, Pdoi^0'=Pdoi^post2, pc^0'=pc^post2, d44^0'=d44^post2, tmp55^0'=tmp55^post2, a88^0'=a88^post2, (-set^post2+set^0 == 0 /\ -DName^post2+DName^0 == 0 /\ PdoType^0-PdoType^post2 == 0 /\ a1111^0-a1111^post2 == 0 /\ -ret_IoCreateDevice1010^post2+ret_IoCreateDevice1010^0 == 0 /\ -pc^post2+pc^0 == 0 /\ -Pdoi^post2+Pdoi^0 == 0 /\ status^0-status^post2 == 0 /\ i^0-i^post2 == 0 /\ tmp99^0-tmp99^post2 == 0 /\ -d44^post2+d44^0 == 0 /\ num^0-num^post2 == 0 /\ c33^0-c33^post2 == 0 /\ -a77^post2+a77^0 == 0 /\ b22^0-b22^post2 == 0 /\ -tmp55^post2+tmp55^0 == 0 /\ -unset^post2+unset^0 == 0 /\ a11^0-a11^post2 == 0 /\ dcIdi^0-dcIdi^post2 == 0 /\ Pdolen^0-Pdolen^post2 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post2 == 0 /\ -lptNamei^post2+lptNamei^0 == 0 /\ -a88^post2+a88^0 == 0), cost: 1 New rule: l4 -> l2 : TRUE, cost: 1 Applied preprocessing Original rule: l5 -> l4 : a1111^0'=a1111^post3, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post3, i^0'=i^post3, PdoType^0'=PdoType^post3, num^0'=num^post3, c33^0'=c33^post3, unset^0'=unset^post3, status^0'=status^post3, a77^0'=a77^post3, Pdolen^0'=Pdolen^post3, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post3, dcIdi^0'=dcIdi^post3, tmp99^0'=tmp99^post3, DName^0'=DName^post3, b22^0'=b22^post3, a11^0'=a11^post3, set^0'=set^post3, lptNamei^0'=lptNamei^post3, Pdoi^0'=Pdoi^post3, pc^0'=pc^post3, d44^0'=d44^post3, tmp55^0'=tmp55^post3, a88^0'=a88^post3, (-a77^post3+a77^0 == 0 /\ -set^post3+set^0 == 0 /\ a1111^0-a1111^post3 == 0 /\ b22^0-b22^post3 == 0 /\ unset^0-unset^post3 == 0 /\ -pc^post3+pc^0 == 0 /\ -1+status^0 <= 0 /\ i^0-i^post3 == 0 /\ -DName^post3+DName^0 == 0 /\ PdoType^0-PdoType^post3 == 0 /\ dcIdi^0-dcIdi^post3 == 0 /\ status^0-status^post3 == 0 /\ -d44^post3+d44^0 == 0 /\ c33^0-c33^post3 == 0 /\ -a11^post3+a11^0 == 0 /\ -tmp55^post3+tmp55^0 == 0 /\ -tmp99^post3+tmp99^0 == 0 /\ -Pdolen^post3+Pdolen^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post3 == 0 /\ -Pdoi^post3+Pdoi^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post3 == 0 /\ -num^post3+num^0 == 0 /\ lptNamei^0-lptNamei^post3 == 0 /\ -a88^post3+a88^0 == 0), cost: 1 New rule: l5 -> l4 : -1+status^0 <= 0, cost: 1 Applied preprocessing Original rule: l5 -> l4 : a1111^0'=a1111^post4, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post4, i^0'=i^post4, PdoType^0'=PdoType^post4, num^0'=num^post4, c33^0'=c33^post4, unset^0'=unset^post4, status^0'=status^post4, a77^0'=a77^post4, Pdolen^0'=Pdolen^post4, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post4, dcIdi^0'=dcIdi^post4, tmp99^0'=tmp99^post4, DName^0'=DName^post4, b22^0'=b22^post4, a11^0'=a11^post4, set^0'=set^post4, lptNamei^0'=lptNamei^post4, Pdoi^0'=Pdoi^post4, pc^0'=pc^post4, d44^0'=d44^post4, tmp55^0'=tmp55^post4, a88^0'=a88^post4, (-a77^post4+a77^0 == 0 /\ -a88^post4+a88^0 == 0 /\ -a11^post4+a11^0 == 0 /\ Pdoi^0-Pdoi^post4 == 0 /\ -d44^post4+d44^0 == 0 /\ i^0-i^post4 == 0 /\ -tmp55^post4+tmp55^0 == 0 /\ unset^0-unset^post4 == 0 /\ -tmp99^post4+tmp99^0 == 0 /\ 3-status^0 <= 0 /\ b22^0-b22^post4 == 0 /\ a1111^0-a1111^post4 == 0 /\ PdoType^0-PdoType^post4 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post4 == 0 /\ lptNamei^0-lptNamei^post4 == 0 /\ dcIdi^0-dcIdi^post4 == 0 /\ status^0-status^post4 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post4 == 0 /\ -Pdolen^post4+Pdolen^0 == 0 /\ -num^post4+num^0 == 0 /\ -DName^post4+DName^0 == 0 /\ -pc^post4+pc^0 == 0 /\ -c33^post4+c33^0 == 0 /\ -set^post4+set^0 == 0), cost: 1 New rule: l5 -> l4 : -3+status^0 >= 0, cost: 1 Applied preprocessing Original rule: l5 -> l4 : a1111^0'=a1111^post5, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post5, i^0'=i^post5, PdoType^0'=PdoType^post5, num^0'=num^post5, c33^0'=c33^post5, unset^0'=unset^post5, status^0'=status^post5, a77^0'=a77^post5, Pdolen^0'=Pdolen^post5, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post5, dcIdi^0'=dcIdi^post5, tmp99^0'=tmp99^post5, DName^0'=DName^post5, b22^0'=b22^post5, a11^0'=a11^post5, set^0'=set^post5, lptNamei^0'=lptNamei^post5, Pdoi^0'=Pdoi^post5, pc^0'=pc^post5, d44^0'=d44^post5, tmp55^0'=tmp55^post5, a88^0'=a88^post5, (-dcIdi^post5+dcIdi^0 == 0 /\ b22^0-b22^post5 == 0 /\ -tmp99^post5+tmp99^0 == 0 /\ -tmp55^post5+tmp55^0 == 0 /\ 2-status^0 <= 0 /\ -Pdoi^post5+Pdoi^0 == 0 /\ -a11^post5+a11^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post5 == 0 /\ -d44^post5+d44^0 == 0 /\ -Pdolen^post5+Pdolen^0 == 0 /\ -a88^post5+a88^0 == 0 /\ -set^post5+set^0 == 0 /\ unset^0-unset^post5 == 0 /\ PdoType^0-PdoType^post5 == 0 /\ -a77^post5+a77^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post5 == 0 /\ lptNamei^0-lptNamei^post5 == 0 /\ -2+status^0 <= 0 /\ -1-num^0+num^post5 == 0 /\ i^0-i^post5 == 0 /\ -DName^post5+DName^0 == 0 /\ -DName^0+a1111^post5 == 0 /\ -pc^post5+pc^0 == 0 /\ status^0-status^post5 == 0 /\ c33^0-c33^post5 == 0), cost: 1 New rule: l5 -> l4 : a1111^0'=DName^0, num^0'=1+num^0, -2+status^0 == 0, cost: 1 Applied preprocessing Original rule: l6 -> l5 : a1111^0'=a1111^post6, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post6, i^0'=i^post6, PdoType^0'=PdoType^post6, num^0'=num^post6, c33^0'=c33^post6, unset^0'=unset^post6, status^0'=status^post6, a77^0'=a77^post6, Pdolen^0'=Pdolen^post6, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post6, dcIdi^0'=dcIdi^post6, tmp99^0'=tmp99^post6, DName^0'=DName^post6, b22^0'=b22^post6, a11^0'=a11^post6, set^0'=set^post6, lptNamei^0'=lptNamei^post6, Pdoi^0'=Pdoi^post6, pc^0'=pc^post6, d44^0'=d44^post6, tmp55^0'=tmp55^post6, a88^0'=a88^post6, (Pdoi^post6 == 0 /\ Pdolen^0-Pdolen^post6 == 0 /\ -dcIdi^post6+dcIdi^0 == 0 /\ -lptNamei^post6+lptNamei^0 == 0 /\ a77^0-a77^post6 == 0 /\ -a88^post6+a88^0 == 0 /\ -b22^post6+b22^0 == 0 /\ i^0-i^post6 == 0 /\ -d44^post6+d44^0 == 0 /\ -set^post6+set^0 == 0 /\ -tmp99^post6+tmp99^0 == 0 /\ status^0-status^post6 == 0 /\ -tmp55^post6+tmp55^0 == 0 /\ -pc^post6+pc^0 == 0 /\ c33^0-c33^post6 == 0 /\ -ret_PPMakeDeviceName66^post6+ret_PPMakeDeviceName66^0 == 0 /\ DName^0-DName^post6 == 0 /\ a1111^0-a1111^post6 == 0 /\ unset^0-unset^post6 == 0 /\ PdoType^0-PdoType^post6 == 0 /\ -a11^post6+a11^0 == 0 /\ num^0-num^post6 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post6 == 0), cost: 1 New rule: l6 -> l5 : Pdoi^0'=0, TRUE, cost: 1 Applied preprocessing Original rule: l7 -> l8 : a1111^0'=a1111^post7, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post7, i^0'=i^post7, PdoType^0'=PdoType^post7, num^0'=num^post7, c33^0'=c33^post7, unset^0'=unset^post7, status^0'=status^post7, a77^0'=a77^post7, Pdolen^0'=Pdolen^post7, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post7, dcIdi^0'=dcIdi^post7, tmp99^0'=tmp99^post7, DName^0'=DName^post7, b22^0'=b22^post7, a11^0'=a11^post7, set^0'=set^post7, lptNamei^0'=lptNamei^post7, Pdoi^0'=Pdoi^post7, pc^0'=pc^post7, d44^0'=d44^post7, tmp55^0'=tmp55^post7, a88^0'=a88^post7, (-ret_IoCreateDevice1010^post7+ret_IoCreateDevice1010^0 == 0 /\ -pc^post7+pc^0 == 0 /\ a1111^0-a1111^post7 == 0 /\ unset^0-unset^post7 == 0 /\ -set^post7+set^0 == 0 /\ -status^post7+status^0 == 0 /\ Pdolen^0-Pdolen^post7 == 0 /\ DName^0-DName^post7 == 0 /\ -b22^post7+b22^0 == 0 /\ c33^0-c33^post7 == 0 /\ 1-status^0 <= 0 /\ -1+status^0 <= 0 /\ -d44^post7+d44^0 == 0 /\ -Pdoi^post7+Pdoi^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post7 == 0 /\ -1-i^0+i^post7 == 0 /\ a77^0-a77^post7 == 0 /\ dcIdi^0-dcIdi^post7 == 0 /\ num^0-num^post7 == 0 /\ -a11^post7+a11^0 == 0 /\ -tmp55^post7+tmp55^0 == 0 /\ -PdoType^post7+PdoType^0 == 0 /\ -a88^post7+a88^0 == 0 /\ tmp99^0-tmp99^post7 == 0 /\ -lptNamei^post7+lptNamei^0 == 0), cost: 1 New rule: l7 -> l8 : i^0'=1+i^0, -1+status^0 == 0, cost: 1 Applied preprocessing Original rule: l7 -> l6 : a1111^0'=a1111^post8, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post8, i^0'=i^post8, PdoType^0'=PdoType^post8, num^0'=num^post8, c33^0'=c33^post8, unset^0'=unset^post8, status^0'=status^post8, a77^0'=a77^post8, Pdolen^0'=Pdolen^post8, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post8, dcIdi^0'=dcIdi^post8, tmp99^0'=tmp99^post8, DName^0'=DName^post8, b22^0'=b22^post8, a11^0'=a11^post8, set^0'=set^post8, lptNamei^0'=lptNamei^post8, Pdoi^0'=Pdoi^post8, pc^0'=pc^post8, d44^0'=d44^post8, tmp55^0'=tmp55^post8, a88^0'=a88^post8, (c33^0-c33^post8 == 0 /\ -PdoType^post8+PdoType^0 == 0 /\ -pc^post8+pc^0 == 0 /\ unset^0-unset^post8 == 0 /\ -status^post8+status^0 == 0 /\ -ret_IoCreateDevice1010^post8+ret_IoCreateDevice1010^0 == 0 /\ num^0-num^post8 == 0 /\ a11^0-a11^post8 == 0 /\ a1111^0-a1111^post8 == 0 /\ status^0 <= 0 /\ DName^0-DName^post8 == 0 /\ Pdolen^0-Pdolen^post8 == 0 /\ -tmp55^post8+tmp55^0 == 0 /\ -Pdoi^post8+Pdoi^0 == 0 /\ -b22^post8+b22^0 == 0 /\ a77^0-a77^post8 == 0 /\ dcIdi^0-dcIdi^post8 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post8 == 0 /\ i^0-i^post8 == 0 /\ tmp99^0-tmp99^post8 == 0 /\ -a88^post8+a88^0 == 0 /\ -lptNamei^post8+lptNamei^0 == 0 /\ -d44^post8+d44^0 == 0 /\ set^0-set^post8 == 0), cost: 1 New rule: l7 -> l6 : status^0 <= 0, cost: 1 Applied preprocessing Original rule: l7 -> l6 : a1111^0'=a1111^post9, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post9, i^0'=i^post9, PdoType^0'=PdoType^post9, num^0'=num^post9, c33^0'=c33^post9, unset^0'=unset^post9, status^0'=status^post9, a77^0'=a77^post9, Pdolen^0'=Pdolen^post9, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post9, dcIdi^0'=dcIdi^post9, tmp99^0'=tmp99^post9, DName^0'=DName^post9, b22^0'=b22^post9, a11^0'=a11^post9, set^0'=set^post9, lptNamei^0'=lptNamei^post9, Pdoi^0'=Pdoi^post9, pc^0'=pc^post9, d44^0'=d44^post9, tmp55^0'=tmp55^post9, a88^0'=a88^post9, (pc^0-pc^post9 == 0 /\ dcIdi^0-dcIdi^post9 == 0 /\ -d44^post9+d44^0 == 0 /\ -a88^post9+a88^0 == 0 /\ -a77^post9+a77^0 == 0 /\ 2-status^0 <= 0 /\ -unset^post9+unset^0 == 0 /\ -Pdoi^post9+Pdoi^0 == 0 /\ tmp99^0-tmp99^post9 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post9 == 0 /\ -tmp55^post9+tmp55^0 == 0 /\ a11^0-a11^post9 == 0 /\ -lptNamei^post9+lptNamei^0 == 0 /\ Pdolen^0-Pdolen^post9 == 0 /\ -status^post9+status^0 == 0 /\ -DName^post9+DName^0 == 0 /\ i^0-i^post9 == 0 /\ -ret_IoCreateDevice1010^post9+ret_IoCreateDevice1010^0 == 0 /\ set^0-set^post9 == 0 /\ num^0-num^post9 == 0 /\ c33^0-c33^post9 == 0 /\ -b22^post9+b22^0 == 0 /\ a1111^0-a1111^post9 == 0 /\ PdoType^0-PdoType^post9 == 0), cost: 1 New rule: l7 -> l6 : -2+status^0 >= 0, cost: 1 Applied preprocessing Original rule: l8 -> l9 : a1111^0'=a1111^post10, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post10, i^0'=i^post10, PdoType^0'=PdoType^post10, num^0'=num^post10, c33^0'=c33^post10, unset^0'=unset^post10, status^0'=status^post10, a77^0'=a77^post10, Pdolen^0'=Pdolen^post10, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post10, dcIdi^0'=dcIdi^post10, tmp99^0'=tmp99^post10, DName^0'=DName^post10, b22^0'=b22^post10, a11^0'=a11^post10, set^0'=set^post10, lptNamei^0'=lptNamei^post10, Pdoi^0'=Pdoi^post10, pc^0'=pc^post10, d44^0'=d44^post10, tmp55^0'=tmp55^post10, a88^0'=a88^post10, (pc^0-pc^post10 == 0 /\ -lptNamei^post10+lptNamei^0 == 0 /\ -a88^post10+a88^0 == 0 /\ a1111^0-a1111^post10 == 0 /\ -d44^post10+d44^0 == 0 /\ PdoType^0-PdoType^post10 == 0 /\ -tmp55^post10+tmp55^0 == 0 /\ -Pdolen^post10+Pdolen^0 == 0 /\ -Pdoi^post10+Pdoi^0 == 0 /\ -ret_IoCreateDevice1010^post10+ret_IoCreateDevice1010^0 == 0 /\ tmp99^0-tmp99^post10 == 0 /\ status^0-status^post10 == 0 /\ -a77^post10+a77^0 == 0 /\ b22^0-b22^post10 == 0 /\ -unset^post10+unset^0 == 0 /\ num^0-num^post10 == 0 /\ i^0-i^post10 == 0 /\ set^0-set^post10 == 0 /\ a11^0-a11^post10 == 0 /\ c33^0-c33^post10 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post10 == 0 /\ -DName^post10+DName^0 == 0 /\ dcIdi^0-dcIdi^post10 == 0), cost: 1 New rule: l8 -> l9 : TRUE, cost: 1 Applied preprocessing Original rule: l10 -> l7 : a1111^0'=a1111^post11, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post11, i^0'=i^post11, PdoType^0'=PdoType^post11, num^0'=num^post11, c33^0'=c33^post11, unset^0'=unset^post11, status^0'=status^post11, a77^0'=a77^post11, Pdolen^0'=Pdolen^post11, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post11, dcIdi^0'=dcIdi^post11, tmp99^0'=tmp99^post11, DName^0'=DName^post11, b22^0'=b22^post11, a11^0'=a11^post11, set^0'=set^post11, lptNamei^0'=lptNamei^post11, Pdoi^0'=Pdoi^post11, pc^0'=pc^post11, d44^0'=d44^post11, tmp55^0'=tmp55^post11, a88^0'=a88^post11, (0 == 0 /\ -tmp99^post11+ret_IoCreateDevice1010^post11 == 0 /\ a77^post11-DName^0 == 0 /\ -d44^post11+d44^0 == 0 /\ dcIdi^0-dcIdi^post11 == 0 /\ -unset^post11+unset^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post11 == 0 /\ a88^post11-Pdoi^0 == 0 /\ -Pdolen^post11+Pdolen^0 == 0 /\ -tmp55^post11+tmp55^0 == 0 /\ set^0-set^post11 == 0 /\ i^0-i^post11 == 0 /\ -lptNamei^post11+lptNamei^0 == 0 /\ b22^0-b22^post11 == 0 /\ DName^0 <= 0 /\ -DName^post11+DName^0 == 0 /\ -ret_IoCreateDevice1010^post11+status^post11 == 0 /\ c33^0-c33^post11 == 0 /\ num^0-num^post11 == 0 /\ -Pdoi^post11+Pdoi^0 == 0 /\ a11^0-a11^post11 == 0 /\ PdoType^0-PdoType^post11 == 0 /\ -1+pc^10 == 0 /\ pc^post11 == 0 /\ a1111^0-a1111^post11 == 0), cost: 1 New rule: l10 -> l7 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, DName^0 <= 0, cost: 1 Applied preprocessing Original rule: l10 -> l2 : a1111^0'=a1111^post12, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post12, i^0'=i^post12, PdoType^0'=PdoType^post12, num^0'=num^post12, c33^0'=c33^post12, unset^0'=unset^post12, status^0'=status^post12, a77^0'=a77^post12, Pdolen^0'=Pdolen^post12, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post12, dcIdi^0'=dcIdi^post12, tmp99^0'=tmp99^post12, DName^0'=DName^post12, b22^0'=b22^post12, a11^0'=a11^post12, set^0'=set^post12, lptNamei^0'=lptNamei^post12, Pdoi^0'=Pdoi^post12, pc^0'=pc^post12, d44^0'=d44^post12, tmp55^0'=tmp55^post12, a88^0'=a88^post12, (status^0-status^post12 == 0 /\ -DName^post12+DName^0 == 0 /\ -a88^post12+a88^0 == 0 /\ Pdoi^0-Pdoi^post12 == 0 /\ dcIdi^0-dcIdi^post12 == 0 /\ i^0-i^post12 == 0 /\ -a77^post12+a77^0 == 0 /\ -tmp55^post12+tmp55^0 == 0 /\ -unset^post12+unset^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post12 == 0 /\ -ret_IoCreateDevice1010^post12+ret_IoCreateDevice1010^0 == 0 /\ -set^post12+set^0 == 0 /\ tmp99^0-tmp99^post12 == 0 /\ -d44^post12+d44^0 == 0 /\ b22^0-b22^post12 == 0 /\ c33^0-c33^post12 == 0 /\ a11^0-a11^post12 == 0 /\ -pc^post12+pc^0 == 0 /\ num^0-num^post12 == 0 /\ Pdolen^0-Pdolen^post12 == 0 /\ 1-DName^0 <= 0 /\ PdoType^0-PdoType^post12 == 0 /\ -lptNamei^post12+lptNamei^0 == 0 /\ a1111^0-a1111^post12 == 0), cost: 1 New rule: l10 -> l2 : -1+DName^0 >= 0, cost: 1 Applied preprocessing Original rule: l3 -> l11 : a1111^0'=a1111^post13, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post13, i^0'=i^post13, PdoType^0'=PdoType^post13, num^0'=num^post13, c33^0'=c33^post13, unset^0'=unset^post13, status^0'=status^post13, a77^0'=a77^post13, Pdolen^0'=Pdolen^post13, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post13, dcIdi^0'=dcIdi^post13, tmp99^0'=tmp99^post13, DName^0'=DName^post13, b22^0'=b22^post13, a11^0'=a11^post13, set^0'=set^post13, lptNamei^0'=lptNamei^post13, Pdoi^0'=Pdoi^post13, pc^0'=pc^post13, d44^0'=d44^post13, tmp55^0'=tmp55^post13, a88^0'=a88^post13, (-a77^post13+a77^0 == 0 /\ -d44^post13+d44^0 == 0 /\ -a88^post13+a88^0 == 0 /\ Pdoi^0-Pdoi^post13 == 0 /\ i^0-i^post13 == 0 /\ -tmp55^post13+tmp55^0 == 0 /\ unset^0-unset^post13 == 0 /\ -Pdolen^post13+Pdolen^0 == 0 /\ -lptNamei^post13+lptNamei^0 == 0 /\ a1111^0-a1111^post13 == 0 /\ -set^post13+set^0 == 0 /\ b22^0-b22^post13 == 0 /\ PdoType^0-PdoType^post13 == 0 /\ dcIdi^0-dcIdi^post13 == 0 /\ status^0-status^post13 == 0 /\ -ret_IoCreateDevice1010^post13+ret_IoCreateDevice1010^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post13 == 0 /\ -num^post13+num^0 == 0 /\ -pc^post13+pc^0 == 0 /\ a11^0-a11^post13 == 0 /\ -c33^post13+c33^0 == 0 /\ -tmp99^post13+tmp99^0 == 0 /\ -DName^post13+DName^0 == 0), cost: 1 New rule: l3 -> l11 : TRUE, cost: 1 Applied preprocessing Original rule: l11 -> l3 : a1111^0'=a1111^post14, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post14, i^0'=i^post14, PdoType^0'=PdoType^post14, num^0'=num^post14, c33^0'=c33^post14, unset^0'=unset^post14, status^0'=status^post14, a77^0'=a77^post14, Pdolen^0'=Pdolen^post14, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post14, dcIdi^0'=dcIdi^post14, tmp99^0'=tmp99^post14, DName^0'=DName^post14, b22^0'=b22^post14, a11^0'=a11^post14, set^0'=set^post14, lptNamei^0'=lptNamei^post14, Pdoi^0'=Pdoi^post14, pc^0'=pc^post14, d44^0'=d44^post14, tmp55^0'=tmp55^post14, a88^0'=a88^post14, (b22^0-b22^post14 == 0 /\ -a88^post14+a88^0 == 0 /\ -dcIdi^post14+dcIdi^0 == 0 /\ Pdoi^0-Pdoi^post14 == 0 /\ -a11^post14+a11^0 == 0 /\ -num^post14+num^0 == 0 /\ -d44^post14+d44^0 == 0 /\ i^0-i^post14 == 0 /\ -tmp55^post14+tmp55^0 == 0 /\ -tmp99^post14+tmp99^0 == 0 /\ -Pdolen^post14+Pdolen^0 == 0 /\ PdoType^0-PdoType^post14 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post14 == 0 /\ -set^post14+set^0 == 0 /\ a1111^0-a1111^post14 == 0 /\ -a77^post14+a77^0 == 0 /\ unset^0-unset^post14 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post14 == 0 /\ lptNamei^0-lptNamei^post14 == 0 /\ -DName^post14+DName^0 == 0 /\ -pc^post14+pc^0 == 0 /\ status^0-status^post14 == 0 /\ -c33^post14+c33^0 == 0), cost: 1 New rule: l11 -> l3 : TRUE, cost: 1 Applied preprocessing Original rule: l9 -> l10 : a1111^0'=a1111^post15, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post15, i^0'=i^post15, PdoType^0'=PdoType^post15, num^0'=num^post15, c33^0'=c33^post15, unset^0'=unset^post15, status^0'=status^post15, a77^0'=a77^post15, Pdolen^0'=Pdolen^post15, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post15, dcIdi^0'=dcIdi^post15, tmp99^0'=tmp99^post15, DName^0'=DName^post15, b22^0'=b22^post15, a11^0'=a11^post15, set^0'=set^post15, lptNamei^0'=lptNamei^post15, Pdoi^0'=Pdoi^post15, pc^0'=pc^post15, d44^0'=d44^post15, tmp55^0'=tmp55^post15, a88^0'=a88^post15, (0 == 0 /\ -dcIdi^post15+dcIdi^0 == 0 /\ ret_PPMakeDeviceName66^post15-tmp55^post15 == 0 /\ 1+i^0-Pdolen^0 <= 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post15 == 0 /\ -num^post15+num^0 == 0 /\ -Pdolen^post15+Pdolen^0 == 0 /\ Pdoi^0-Pdoi^post15 == 0 /\ -set^post15+set^0 == 0 /\ unset^0-unset^post15 == 0 /\ PdoType^0-PdoType^post15 == 0 /\ -a77^post15+a77^0 == 0 /\ -pc^post15+pc^0 == 0 /\ -tmp99^post15+tmp99^0 == 0 /\ -PdoType^0+b22^post15 == 0 /\ a1111^0-a1111^post15 == 0 /\ -a88^post15+a88^0 == 0 /\ DName^post15-ret_PPMakeDeviceName66^post15 == 0 /\ c33^post15-dcIdi^0 == 0 /\ -lptNamei^post15+lptNamei^0 == 0 /\ status^0-status^post15 == 0 /\ a11^post15-lptNamei^0 == 0 /\ i^0-i^post15 == 0 /\ -num^0+d44^post15 == 0), cost: 1 New rule: l9 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 1 Applied preprocessing Original rule: l9 -> l2 : a1111^0'=a1111^post16, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post16, i^0'=i^post16, PdoType^0'=PdoType^post16, num^0'=num^post16, c33^0'=c33^post16, unset^0'=unset^post16, status^0'=status^post16, a77^0'=a77^post16, Pdolen^0'=Pdolen^post16, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post16, dcIdi^0'=dcIdi^post16, tmp99^0'=tmp99^post16, DName^0'=DName^post16, b22^0'=b22^post16, a11^0'=a11^post16, set^0'=set^post16, lptNamei^0'=lptNamei^post16, Pdoi^0'=Pdoi^post16, pc^0'=pc^post16, d44^0'=d44^post16, tmp55^0'=tmp55^post16, a88^0'=a88^post16, (d44^0-d44^post16 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post16 == 0 /\ status^0-status^post16 == 0 /\ i^0-i^post16 == 0 /\ -a88^post16+a88^0 == 0 /\ -i^0+Pdolen^0 <= 0 /\ -tmp55^post16+tmp55^0 == 0 /\ unset^0-unset^post16 == 0 /\ -Pdolen^post16+Pdolen^0 == 0 /\ PdoType^0-PdoType^post16 == 0 /\ -a11^post16+a11^0 == 0 /\ -dcIdi^post16+dcIdi^0 == 0 /\ -pc^post16+pc^0 == 0 /\ -tmp99^post16+tmp99^0 == 0 /\ -lptNamei^post16+lptNamei^0 == 0 /\ -b22^post16+b22^0 == 0 /\ c33^0-c33^post16 == 0 /\ -ret_PPMakeDeviceName66^post16+ret_PPMakeDeviceName66^0 == 0 /\ a1111^0-a1111^post16 == 0 /\ -set^post16+set^0 == 0 /\ -Pdoi^post16+Pdoi^0 == 0 /\ num^0-num^post16 == 0 /\ a77^0-a77^post16 == 0 /\ DName^0-DName^post16 == 0), cost: 1 New rule: l9 -> l2 : -i^0+Pdolen^0 <= 0, cost: 1 Applied preprocessing Original rule: l12 -> l8 : a1111^0'=a1111^post17, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post17, i^0'=i^post17, PdoType^0'=PdoType^post17, num^0'=num^post17, c33^0'=c33^post17, unset^0'=unset^post17, status^0'=status^post17, a77^0'=a77^post17, Pdolen^0'=Pdolen^post17, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post17, dcIdi^0'=dcIdi^post17, tmp99^0'=tmp99^post17, DName^0'=DName^post17, b22^0'=b22^post17, a11^0'=a11^post17, set^0'=set^post17, lptNamei^0'=lptNamei^post17, Pdoi^0'=Pdoi^post17, pc^0'=pc^post17, d44^0'=d44^post17, tmp55^0'=tmp55^post17, a88^0'=a88^post17, (status^0-status^post17 == 0 /\ PdoType^0-PdoType^post17 == 0 /\ a77^0-a77^post17 == 0 /\ -tmp55^post17+tmp55^0 == 0 /\ -1+set^20 == 0 /\ i^0-i^post17 == 0 /\ -tmp99^post17+tmp99^0 == 0 /\ -Pdoi^post17+Pdoi^0 == 0 /\ unset^post17 == 0 /\ -b22^post17+b22^0 == 0 /\ a1111^0-a1111^post17 == 0 /\ -d44^post17+d44^0 == 0 /\ pc^0-pc^post17 == 0 /\ set^10-unset^post17 == 0 /\ num^0-num^post17 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post17 == 0 /\ -a11^post17+a11^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post17 == 0 /\ Pdolen^0-Pdolen^post17 == 0 /\ -dcIdi^post17+dcIdi^0 == 0 /\ DName^0-DName^post17 == 0 /\ -a88^post17+a88^0 == 0 /\ set^post17 == 0 /\ -lptNamei^post17+lptNamei^0 == 0 /\ -c33^post17+c33^0 == 0), cost: 1 New rule: l12 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 1 Applied preprocessing Original rule: l13 -> l12 : a1111^0'=a1111^post18, ret_PPMakeDeviceName66^0'=ret_PPMakeDeviceName66^post18, i^0'=i^post18, PdoType^0'=PdoType^post18, num^0'=num^post18, c33^0'=c33^post18, unset^0'=unset^post18, status^0'=status^post18, a77^0'=a77^post18, Pdolen^0'=Pdolen^post18, ret_IoCreateDevice1010^0'=ret_IoCreateDevice1010^post18, dcIdi^0'=dcIdi^post18, tmp99^0'=tmp99^post18, DName^0'=DName^post18, b22^0'=b22^post18, a11^0'=a11^post18, set^0'=set^post18, lptNamei^0'=lptNamei^post18, Pdoi^0'=Pdoi^post18, pc^0'=pc^post18, d44^0'=d44^post18, tmp55^0'=tmp55^post18, a88^0'=a88^post18, (-PdoType^post18+PdoType^0 == 0 /\ -status^post18+status^0 == 0 /\ -set^post18+set^0 == 0 /\ unset^0-unset^post18 == 0 /\ -a11^post18+a11^0 == 0 /\ -pc^post18+pc^0 == 0 /\ num^0-num^post18 == 0 /\ c33^0-c33^post18 == 0 /\ i^0-i^post18 == 0 /\ a1111^0-a1111^post18 == 0 /\ DName^0-DName^post18 == 0 /\ Pdolen^0-Pdolen^post18 == 0 /\ -b22^post18+b22^0 == 0 /\ a77^0-a77^post18 == 0 /\ -lptNamei^post18+lptNamei^0 == 0 /\ -d44^post18+d44^0 == 0 /\ tmp99^0-tmp99^post18 == 0 /\ -tmp55^post18+tmp55^0 == 0 /\ ret_PPMakeDeviceName66^0-ret_PPMakeDeviceName66^post18 == 0 /\ -Pdoi^post18+Pdoi^0 == 0 /\ ret_IoCreateDevice1010^0-ret_IoCreateDevice1010^post18 == 0 /\ -dcIdi^post18+dcIdi^0 == 0 /\ -a88^post18+a88^0 == 0), cost: 1 New rule: l13 -> l12 : TRUE, cost: 1 Simplified rules Start location: l13 19: l2 -> l3 : num^0'=0, unset^0'=0, TRUE, cost: 1 31: l3 -> l11 : TRUE, cost: 1 20: l4 -> l2 : TRUE, cost: 1 21: l5 -> l4 : -1+status^0 <= 0, cost: 1 22: l5 -> l4 : -3+status^0 >= 0, cost: 1 23: l5 -> l4 : a1111^0'=DName^0, num^0'=1+num^0, -2+status^0 == 0, cost: 1 24: l6 -> l5 : Pdoi^0'=0, TRUE, cost: 1 25: l7 -> l8 : i^0'=1+i^0, -1+status^0 == 0, cost: 1 26: l7 -> l6 : status^0 <= 0, cost: 1 27: l7 -> l6 : -2+status^0 >= 0, cost: 1 28: l8 -> l9 : TRUE, cost: 1 33: l9 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 1 34: l9 -> l2 : -i^0+Pdolen^0 <= 0, cost: 1 29: l10 -> l7 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, DName^0 <= 0, cost: 1 30: l10 -> l2 : -1+DName^0 >= 0, cost: 1 32: l11 -> l3 : TRUE, cost: 1 35: l12 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 1 36: l13 -> l12 : TRUE, cost: 1 Eliminating location l12 by chaining: Applied chaining First rule: l13 -> l12 : TRUE, cost: 1 Second rule: l12 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 1 New rule: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Applied deletion Removed the following rules: 35 36 Eliminating location l11 by chaining: Applied chaining First rule: l3 -> l11 : TRUE, cost: 1 Second rule: l11 -> l3 : TRUE, cost: 1 New rule: l3 -> l3 : TRUE, cost: 2 Applied deletion Removed the following rules: 31 32 Eliminated locations on linear paths Start location: l13 19: l2 -> l3 : num^0'=0, unset^0'=0, TRUE, cost: 1 38: l3 -> l3 : TRUE, cost: 2 20: l4 -> l2 : TRUE, cost: 1 21: l5 -> l4 : -1+status^0 <= 0, cost: 1 22: l5 -> l4 : -3+status^0 >= 0, cost: 1 23: l5 -> l4 : a1111^0'=DName^0, num^0'=1+num^0, -2+status^0 == 0, cost: 1 24: l6 -> l5 : Pdoi^0'=0, TRUE, cost: 1 25: l7 -> l8 : i^0'=1+i^0, -1+status^0 == 0, cost: 1 26: l7 -> l6 : status^0 <= 0, cost: 1 27: l7 -> l6 : -2+status^0 >= 0, cost: 1 28: l8 -> l9 : TRUE, cost: 1 33: l9 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 1 34: l9 -> l2 : -i^0+Pdolen^0 <= 0, cost: 1 29: l10 -> l7 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, DName^0 <= 0, cost: 1 30: l10 -> l2 : -1+DName^0 >= 0, cost: 1 37: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Applied nonterm Original rule: l3 -> l3 : TRUE, cost: 2 New rule: l3 -> [14] : n >= 0, cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_blijKF.txt Applied deletion Removed the following rules: 38 Accelerated simple loops Start location: l13 19: l2 -> l3 : num^0'=0, unset^0'=0, TRUE, cost: 1 39: l3 -> [14] : n >= 0, cost: NONTERM 20: l4 -> l2 : TRUE, cost: 1 21: l5 -> l4 : -1+status^0 <= 0, cost: 1 22: l5 -> l4 : -3+status^0 >= 0, cost: 1 23: l5 -> l4 : a1111^0'=DName^0, num^0'=1+num^0, -2+status^0 == 0, cost: 1 24: l6 -> l5 : Pdoi^0'=0, TRUE, cost: 1 25: l7 -> l8 : i^0'=1+i^0, -1+status^0 == 0, cost: 1 26: l7 -> l6 : status^0 <= 0, cost: 1 27: l7 -> l6 : -2+status^0 >= 0, cost: 1 28: l8 -> l9 : TRUE, cost: 1 33: l9 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 1 34: l9 -> l2 : -i^0+Pdolen^0 <= 0, cost: 1 29: l10 -> l7 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, DName^0 <= 0, cost: 1 30: l10 -> l2 : -1+DName^0 >= 0, cost: 1 37: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Applied chaining First rule: l2 -> l3 : num^0'=0, unset^0'=0, TRUE, cost: 1 Second rule: l3 -> [14] : n >= 0, cost: NONTERM New rule: l2 -> [14] : TRUE, cost: NONTERM Applied deletion Removed the following rules: 39 Chained accelerated rules with incoming rules Start location: l13 19: l2 -> l3 : num^0'=0, unset^0'=0, TRUE, cost: 1 40: l2 -> [14] : TRUE, cost: NONTERM 20: l4 -> l2 : TRUE, cost: 1 21: l5 -> l4 : -1+status^0 <= 0, cost: 1 22: l5 -> l4 : -3+status^0 >= 0, cost: 1 23: l5 -> l4 : a1111^0'=DName^0, num^0'=1+num^0, -2+status^0 == 0, cost: 1 24: l6 -> l5 : Pdoi^0'=0, TRUE, cost: 1 25: l7 -> l8 : i^0'=1+i^0, -1+status^0 == 0, cost: 1 26: l7 -> l6 : status^0 <= 0, cost: 1 27: l7 -> l6 : -2+status^0 >= 0, cost: 1 28: l8 -> l9 : TRUE, cost: 1 33: l9 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 1 34: l9 -> l2 : -i^0+Pdolen^0 <= 0, cost: 1 29: l10 -> l7 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, DName^0 <= 0, cost: 1 30: l10 -> l2 : -1+DName^0 >= 0, cost: 1 37: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l13 40: l2 -> [14] : TRUE, cost: NONTERM 20: l4 -> l2 : TRUE, cost: 1 21: l5 -> l4 : -1+status^0 <= 0, cost: 1 22: l5 -> l4 : -3+status^0 >= 0, cost: 1 23: l5 -> l4 : a1111^0'=DName^0, num^0'=1+num^0, -2+status^0 == 0, cost: 1 24: l6 -> l5 : Pdoi^0'=0, TRUE, cost: 1 25: l7 -> l8 : i^0'=1+i^0, -1+status^0 == 0, cost: 1 26: l7 -> l6 : status^0 <= 0, cost: 1 27: l7 -> l6 : -2+status^0 >= 0, cost: 1 28: l8 -> l9 : TRUE, cost: 1 33: l9 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 1 34: l9 -> l2 : -i^0+Pdolen^0 <= 0, cost: 1 29: l10 -> l7 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, DName^0 <= 0, cost: 1 30: l10 -> l2 : -1+DName^0 >= 0, cost: 1 37: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Eliminating location l9 by chaining: Applied chaining First rule: l8 -> l9 : TRUE, cost: 1 Second rule: l9 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 1 New rule: l8 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 2 Applied chaining First rule: l8 -> l9 : TRUE, cost: 1 Second rule: l9 -> l2 : -i^0+Pdolen^0 <= 0, cost: 1 New rule: l8 -> l2 : -i^0+Pdolen^0 <= 0, cost: 2 Applied deletion Removed the following rules: 28 33 34 Eliminating location l7 by chaining: Applied chaining First rule: l10 -> l7 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, DName^0 <= 0, cost: 1 Second rule: l7 -> l8 : i^0'=1+i^0, -1+status^0 == 0, cost: 1 New rule: l10 -> l8 : i^0'=1+i^0, status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, (-1+status^post11 == 0 /\ DName^0 <= 0), cost: 2 Applied chaining First rule: l10 -> l7 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, DName^0 <= 0, cost: 1 Second rule: l7 -> l6 : status^0 <= 0, cost: 1 New rule: l10 -> l6 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, (status^post11 <= 0 /\ DName^0 <= 0), cost: 2 Applied chaining First rule: l10 -> l7 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, DName^0 <= 0, cost: 1 Second rule: l7 -> l6 : -2+status^0 >= 0, cost: 1 New rule: l10 -> l6 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, (DName^0 <= 0 /\ -2+status^post11 >= 0), cost: 2 Applied deletion Removed the following rules: 25 26 27 29 Eliminating location l5 by chaining: Applied chaining First rule: l6 -> l5 : Pdoi^0'=0, TRUE, cost: 1 Second rule: l5 -> l4 : -1+status^0 <= 0, cost: 1 New rule: l6 -> l4 : Pdoi^0'=0, -1+status^0 <= 0, cost: 2 Applied chaining First rule: l6 -> l5 : Pdoi^0'=0, TRUE, cost: 1 Second rule: l5 -> l4 : -3+status^0 >= 0, cost: 1 New rule: l6 -> l4 : Pdoi^0'=0, -3+status^0 >= 0, cost: 2 Applied chaining First rule: l6 -> l5 : Pdoi^0'=0, TRUE, cost: 1 Second rule: l5 -> l4 : a1111^0'=DName^0, num^0'=1+num^0, -2+status^0 == 0, cost: 1 New rule: l6 -> l4 : a1111^0'=DName^0, num^0'=1+num^0, Pdoi^0'=0, -2+status^0 == 0, cost: 2 Applied deletion Removed the following rules: 21 22 23 24 Eliminated locations on tree-shaped paths Start location: l13 40: l2 -> [14] : TRUE, cost: NONTERM 20: l4 -> l2 : TRUE, cost: 1 46: l6 -> l4 : Pdoi^0'=0, -1+status^0 <= 0, cost: 2 47: l6 -> l4 : Pdoi^0'=0, -3+status^0 >= 0, cost: 2 48: l6 -> l4 : a1111^0'=DName^0, num^0'=1+num^0, Pdoi^0'=0, -2+status^0 == 0, cost: 2 41: l8 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 2 42: l8 -> l2 : -i^0+Pdolen^0 <= 0, cost: 2 30: l10 -> l2 : -1+DName^0 >= 0, cost: 1 43: l10 -> l8 : i^0'=1+i^0, status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, (-1+status^post11 == 0 /\ DName^0 <= 0), cost: 2 44: l10 -> l6 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, (status^post11 <= 0 /\ DName^0 <= 0), cost: 2 45: l10 -> l6 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, (DName^0 <= 0 /\ -2+status^post11 >= 0), cost: 2 37: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Eliminating location l10 by chaining: Applied chaining First rule: l8 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 2 Second rule: l10 -> l2 : -1+DName^0 >= 0, cost: 1 New rule: l8 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 3 Applied chaining First rule: l8 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 2 Second rule: l10 -> l8 : i^0'=1+i^0, status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, (-1+status^post11 == 0 /\ DName^0 <= 0), cost: 2 New rule: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=1+i^0, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1+status^post11 == 0 /\ 1+i^0-Pdolen^0 <= 0 /\ tmp55^post15 <= 0), cost: 4 Applied chaining First rule: l8 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 2 Second rule: l10 -> l6 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, (status^post11 <= 0 /\ DName^0 <= 0), cost: 2 New rule: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 4 Applied chaining First rule: l8 -> l10 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, 1+i^0-Pdolen^0 <= 0, cost: 2 Second rule: l10 -> l6 : status^0'=status^post11, a77^0'=DName^0, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, pc^0'=0, a88^0'=Pdoi^0, (DName^0 <= 0 /\ -2+status^post11 >= 0), cost: 2 New rule: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 4 Applied deletion Removed the following rules: 30 41 43 44 45 Eliminating location l4 by chaining: Applied chaining First rule: l6 -> l4 : Pdoi^0'=0, -1+status^0 <= 0, cost: 2 Second rule: l4 -> l2 : TRUE, cost: 1 New rule: l6 -> l2 : Pdoi^0'=0, -1+status^0 <= 0, cost: 3 Applied chaining First rule: l6 -> l4 : Pdoi^0'=0, -3+status^0 >= 0, cost: 2 Second rule: l4 -> l2 : TRUE, cost: 1 New rule: l6 -> l2 : Pdoi^0'=0, -3+status^0 >= 0, cost: 3 Applied chaining First rule: l6 -> l4 : a1111^0'=DName^0, num^0'=1+num^0, Pdoi^0'=0, -2+status^0 == 0, cost: 2 Second rule: l4 -> l2 : TRUE, cost: 1 New rule: l6 -> l2 : a1111^0'=DName^0, num^0'=1+num^0, Pdoi^0'=0, -2+status^0 == 0, cost: 3 Applied deletion Removed the following rules: 20 46 47 48 Eliminated locations on tree-shaped paths Start location: l13 40: l2 -> [14] : TRUE, cost: NONTERM 53: l6 -> l2 : Pdoi^0'=0, -1+status^0 <= 0, cost: 3 54: l6 -> l2 : Pdoi^0'=0, -3+status^0 >= 0, cost: 3 55: l6 -> l2 : a1111^0'=DName^0, num^0'=1+num^0, Pdoi^0'=0, -2+status^0 == 0, cost: 3 42: l8 -> l2 : -i^0+Pdolen^0 <= 0, cost: 2 49: l8 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 3 50: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=1+i^0, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1+status^post11 == 0 /\ 1+i^0-Pdolen^0 <= 0 /\ tmp55^post15 <= 0), cost: 4 51: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 4 52: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 4 37: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Applied simplification Original rule: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=1+i^0, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1+status^post11 == 0 /\ 1+i^0-Pdolen^0 <= 0 /\ tmp55^post15 <= 0), cost: 4 New rule: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=1+i^0, c33^0'=dcIdi^0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ tmp55^post15 <= 0), cost: 4 Simplified simple loops Start location: l13 40: l2 -> [14] : TRUE, cost: NONTERM 53: l6 -> l2 : Pdoi^0'=0, -1+status^0 <= 0, cost: 3 54: l6 -> l2 : Pdoi^0'=0, -3+status^0 >= 0, cost: 3 55: l6 -> l2 : a1111^0'=DName^0, num^0'=1+num^0, Pdoi^0'=0, -2+status^0 == 0, cost: 3 42: l8 -> l2 : -i^0+Pdolen^0 <= 0, cost: 2 49: l8 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 3 51: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 4 52: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 4 56: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=1+i^0, c33^0'=dcIdi^0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ tmp55^post15 <= 0), cost: 4 37: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Applied acceleration Original rule: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=1+i^0, c33^0'=dcIdi^0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ tmp55^post15 <= 0), cost: 4 New rule: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=i^0+n0, c33^0'=dcIdi^0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-tmp55^post15 >= 0 /\ -i^0+Pdolen^0-n0 >= 0 /\ -1+n0 >= 0), cost: 4*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_AfEOJn.txt Applied instantiation Original rule: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=i^0+n0, c33^0'=dcIdi^0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-tmp55^post15 >= 0 /\ -i^0+Pdolen^0-n0 >= 0 /\ -1+n0 >= 0), cost: 4*n0 New rule: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (0 >= 0 /\ -tmp55^post15 >= 0 /\ -1-i^0+Pdolen^0 >= 0), cost: -4*i^0+4*Pdolen^0 Applied simplification Original rule: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (0 >= 0 /\ -tmp55^post15 >= 0 /\ -1-i^0+Pdolen^0 >= 0), cost: -4*i^0+4*Pdolen^0 New rule: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: -4*i^0+4*Pdolen^0 Applied deletion Removed the following rules: 56 Accelerated simple loops Start location: l13 40: l2 -> [14] : TRUE, cost: NONTERM 53: l6 -> l2 : Pdoi^0'=0, -1+status^0 <= 0, cost: 3 54: l6 -> l2 : Pdoi^0'=0, -3+status^0 >= 0, cost: 3 55: l6 -> l2 : a1111^0'=DName^0, num^0'=1+num^0, Pdoi^0'=0, -2+status^0 == 0, cost: 3 42: l8 -> l2 : -i^0+Pdolen^0 <= 0, cost: 2 49: l8 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 3 51: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 4 52: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 4 58: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: -4*i^0+4*Pdolen^0 37: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Applied chaining First rule: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Second rule: l8 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: -4*i^0+4*Pdolen^0 New rule: l13 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 2-4*i^0+4*Pdolen^0 Applied deletion Removed the following rules: 58 Chained accelerated rules with incoming rules Start location: l13 40: l2 -> [14] : TRUE, cost: NONTERM 53: l6 -> l2 : Pdoi^0'=0, -1+status^0 <= 0, cost: 3 54: l6 -> l2 : Pdoi^0'=0, -3+status^0 >= 0, cost: 3 55: l6 -> l2 : a1111^0'=DName^0, num^0'=1+num^0, Pdoi^0'=0, -2+status^0 == 0, cost: 3 42: l8 -> l2 : -i^0+Pdolen^0 <= 0, cost: 2 49: l8 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 3 51: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 4 52: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 4 37: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 59: l13 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 2-4*i^0+4*Pdolen^0 Eliminating location l8 by chaining: Applied chaining First rule: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Second rule: l8 -> l2 : -i^0+Pdolen^0 <= 0, cost: 2 New rule: l13 -> l2 : unset^0'=0, set^0'=0, -i^0+Pdolen^0 <= 0, cost: 4 Applied chaining First rule: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Second rule: l8 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 3 New rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 5 Applied chaining First rule: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Second rule: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 4 New rule: l13 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 6 Applied chaining First rule: l13 -> l8 : unset^0'=0, set^0'=0, TRUE, cost: 2 Second rule: l8 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 4 New rule: l13 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 6 Applied chaining First rule: l13 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 2-4*i^0+4*Pdolen^0 Second rule: l8 -> l2 : -i^0+Pdolen^0 <= 0, cost: 2 New rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (0 <= 0 /\ -1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 4-4*i^0+4*Pdolen^0 Applied simplification Original rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (0 <= 0 /\ -1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 4-4*i^0+4*Pdolen^0 New rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 4-4*i^0+4*Pdolen^0 Applied partial deletion Original rule: l13 -> l8 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 2-4*i^0+4*Pdolen^0 New rule: l13 -> [16] : (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 2-4*i^0+4*Pdolen^0 Applied deletion Removed the following rules: 37 42 49 51 52 59 Eliminated locations on tree-shaped paths Start location: l13 40: l2 -> [14] : TRUE, cost: NONTERM 53: l6 -> l2 : Pdoi^0'=0, -1+status^0 <= 0, cost: 3 54: l6 -> l2 : Pdoi^0'=0, -3+status^0 >= 0, cost: 3 55: l6 -> l2 : a1111^0'=DName^0, num^0'=1+num^0, Pdoi^0'=0, -2+status^0 == 0, cost: 3 60: l13 -> l2 : unset^0'=0, set^0'=0, -i^0+Pdolen^0 <= 0, cost: 4 61: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 5 62: l13 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 6 63: l13 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 6 64: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 4-4*i^0+4*Pdolen^0 65: l13 -> [16] : (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 2-4*i^0+4*Pdolen^0 Applied pruning (of leafs and parallel rules): Start location: l13 40: l2 -> [14] : TRUE, cost: NONTERM 53: l6 -> l2 : Pdoi^0'=0, -1+status^0 <= 0, cost: 3 54: l6 -> l2 : Pdoi^0'=0, -3+status^0 >= 0, cost: 3 55: l6 -> l2 : a1111^0'=DName^0, num^0'=1+num^0, Pdoi^0'=0, -2+status^0 == 0, cost: 3 60: l13 -> l2 : unset^0'=0, set^0'=0, -i^0+Pdolen^0 <= 0, cost: 4 61: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 5 62: l13 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 6 63: l13 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 6 64: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 4-4*i^0+4*Pdolen^0 Eliminating location l6 by chaining: Applied chaining First rule: l13 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 6 Second rule: l6 -> l2 : Pdoi^0'=0, -1+status^0 <= 0, cost: 3 New rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1+status^post11 <= 0 /\ 1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 9 Applied simplification Original rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1+status^post11 <= 0 /\ 1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 9 New rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 9 Applied chaining First rule: l13 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 6 Second rule: l6 -> l2 : Pdoi^0'=0, -3+status^0 >= 0, cost: 3 New rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -3+status^post11 >= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 9 Applied simplification Original rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -3+status^post11 >= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 9 New rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -3+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 9 Applied chaining First rule: l13 -> l6 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 6 Second rule: l6 -> l2 : a1111^0'=DName^0, num^0'=1+num^0, Pdoi^0'=0, -2+status^0 == 0, cost: 3 New rule: l13 -> l2 : a1111^0'=tmp55^post15, ret_PPMakeDeviceName66^0'=tmp55^post15, num^0'=1+num^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ -2+status^post11 == 0 /\ tmp55^post15 <= 0), cost: 9 Applied simplification Original rule: l13 -> l2 : a1111^0'=tmp55^post15, ret_PPMakeDeviceName66^0'=tmp55^post15, num^0'=1+num^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 >= 0 /\ -2+status^post11 == 0 /\ tmp55^post15 <= 0), cost: 9 New rule: l13 -> l2 : a1111^0'=tmp55^post15, ret_PPMakeDeviceName66^0'=tmp55^post15, num^0'=1+num^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 == 0 /\ tmp55^post15 <= 0), cost: 9 Applied deletion Removed the following rules: 53 54 55 62 63 Eliminated locations on tree-shaped paths Start location: l13 40: l2 -> [14] : TRUE, cost: NONTERM 60: l13 -> l2 : unset^0'=0, set^0'=0, -i^0+Pdolen^0 <= 0, cost: 4 61: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 5 64: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 4-4*i^0+4*Pdolen^0 66: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 9 67: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -3+status^post11 >= 0 /\ tmp55^post15 <= 0), cost: 9 68: l13 -> l2 : a1111^0'=tmp55^post15, ret_PPMakeDeviceName66^0'=tmp55^post15, num^0'=1+num^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 == 0 /\ tmp55^post15 <= 0), cost: 9 Applied pruning (of leafs and parallel rules): Start location: l13 40: l2 -> [14] : TRUE, cost: NONTERM 60: l13 -> l2 : unset^0'=0, set^0'=0, -i^0+Pdolen^0 <= 0, cost: 4 61: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 5 64: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 4-4*i^0+4*Pdolen^0 66: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 9 68: l13 -> l2 : a1111^0'=tmp55^post15, ret_PPMakeDeviceName66^0'=tmp55^post15, num^0'=1+num^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 == 0 /\ tmp55^post15 <= 0), cost: 9 Eliminating location l2 by chaining: Applied chaining First rule: l13 -> l2 : unset^0'=0, set^0'=0, -i^0+Pdolen^0 <= 0, cost: 4 Second rule: l2 -> [14] : TRUE, cost: NONTERM New rule: l13 -> [14] : -i^0+Pdolen^0 <= 0, cost: NONTERM Applied chaining First rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: 5 Second rule: l2 -> [14] : TRUE, cost: NONTERM New rule: l13 -> [14] : (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: NONTERM Applied chaining First rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, i^0'=Pdolen^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=1, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=1, tmp99^0'=1, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: 4-4*i^0+4*Pdolen^0 Second rule: l2 -> [14] : TRUE, cost: NONTERM New rule: l13 -> [14] : (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: NONTERM Applied chaining First rule: l13 -> l2 : ret_PPMakeDeviceName66^0'=tmp55^post15, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: 9 Second rule: l2 -> [14] : TRUE, cost: NONTERM New rule: l13 -> [14] : (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: NONTERM Applied chaining First rule: l13 -> l2 : a1111^0'=tmp55^post15, ret_PPMakeDeviceName66^0'=tmp55^post15, num^0'=1+num^0, c33^0'=dcIdi^0, unset^0'=0, status^0'=status^post11, a77^0'=tmp55^post15, ret_IoCreateDevice1010^0'=status^post11, tmp99^0'=status^post11, DName^0'=tmp55^post15, b22^0'=PdoType^0, a11^0'=lptNamei^0, set^0'=0, Pdoi^0'=0, pc^0'=0, d44^0'=num^0, tmp55^0'=tmp55^post15, a88^0'=Pdoi^0, (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 == 0 /\ tmp55^post15 <= 0), cost: 9 Second rule: l2 -> [14] : TRUE, cost: NONTERM New rule: l13 -> [14] : (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 == 0 /\ tmp55^post15 <= 0), cost: NONTERM Applied deletion Removed the following rules: 40 60 61 64 66 68 Eliminated locations on tree-shaped paths Start location: l13 69: l13 -> [14] : -i^0+Pdolen^0 <= 0, cost: NONTERM 70: l13 -> [14] : (1+i^0-Pdolen^0 <= 0 /\ -1+tmp55^post15 >= 0), cost: NONTERM 71: l13 -> [14] : (-1-i^0+Pdolen^0 >= 0 /\ tmp55^post15 <= 0), cost: NONTERM 72: l13 -> [14] : (1+i^0-Pdolen^0 <= 0 /\ status^post11 <= 0 /\ tmp55^post15 <= 0), cost: NONTERM 73: l13 -> [14] : (1+i^0-Pdolen^0 <= 0 /\ -2+status^post11 == 0 /\ tmp55^post15 <= 0), cost: NONTERM Computing asymptotic complexity Proved nontermination of rule 69 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: -i^0+Pdolen^0 <= 0