MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. eval_ex3_start(v__0,v_b,v_x) -> eval_ex3_bb0_in(v__0,v_b,v_x) True (1,1) 1. eval_ex3_bb0_in(v__0,v_b,v_x) -> eval_ex3_0(v__0,v_b,v_x) True (?,1) 2. eval_ex3_0(v__0,v_b,v_x) -> eval_ex3_1(v__0,v_b,v_x) True (?,1) 3. eval_ex3_1(v__0,v_b,v_x) -> eval_ex3_2(v__0,v_b,v_x) True (?,1) 4. eval_ex3_2(v__0,v_b,v_x) -> eval_ex3_3(v__0,v_b,v_x) True (?,1) 5. eval_ex3_3(v__0,v_b,v_x) -> eval_ex3_4(v__0,v_b,v_x) True (?,1) 6. eval_ex3_4(v__0,v_b,v_x) -> eval_ex3_bb1_in(v_x,v_b,v_x) True (?,1) 7. eval_ex3_bb1_in(v__0,v_b,v_x) -> eval_ex3_bb2_in(v__0,v_b,v_x) [-1 + v__0 >= 0 && 254 >= v__0] (?,1) 8. eval_ex3_bb1_in(v__0,v_b,v_x) -> eval_ex3_bb3_in(v__0,v_b,v_x) [0 >= v__0] (?,1) 9. eval_ex3_bb1_in(v__0,v_b,v_x) -> eval_ex3_bb3_in(v__0,v_b,v_x) [v__0 >= 255] (?,1) 10. eval_ex3_bb2_in(v__0,v_b,v_x) -> eval_ex3_bb1_in(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 >= v_b] (?,1) 11. eval_ex3_bb2_in(v__0,v_b,v_x) -> eval_ex3_bb1_in(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 + v_b >= 0] (?,1) 12. eval_ex3_bb2_in(v__0,v_b,v_x) -> eval_ex3_bb1_in(-1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && v_b = 0] (?,1) 13. eval_ex3_bb3_in(v__0,v_b,v_x) -> eval_ex3_stop(v__0,v_b,v_x) True (?,1) Signature: {(eval_ex3_0,3) ;(eval_ex3_1,3) ;(eval_ex3_2,3) ;(eval_ex3_3,3) ;(eval_ex3_4,3) ;(eval_ex3_bb0_in,3) ;(eval_ex3_bb1_in,3) ;(eval_ex3_bb2_in,3) ;(eval_ex3_bb3_in,3) ;(eval_ex3_start,3) ;(eval_ex3_stop,3)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7,8,9},7->{10,11,12},8->{13},9->{13},10->{7,8,9},11->{7,8 ,9},12->{7,8,9},13->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(10,8),(11,8),(12,9)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. eval_ex3_start(v__0,v_b,v_x) -> eval_ex3_bb0_in(v__0,v_b,v_x) True (1,1) 1. eval_ex3_bb0_in(v__0,v_b,v_x) -> eval_ex3_0(v__0,v_b,v_x) True (?,1) 2. eval_ex3_0(v__0,v_b,v_x) -> eval_ex3_1(v__0,v_b,v_x) True (?,1) 3. eval_ex3_1(v__0,v_b,v_x) -> eval_ex3_2(v__0,v_b,v_x) True (?,1) 4. eval_ex3_2(v__0,v_b,v_x) -> eval_ex3_3(v__0,v_b,v_x) True (?,1) 5. eval_ex3_3(v__0,v_b,v_x) -> eval_ex3_4(v__0,v_b,v_x) True (?,1) 6. eval_ex3_4(v__0,v_b,v_x) -> eval_ex3_bb1_in(v_x,v_b,v_x) True (?,1) 7. eval_ex3_bb1_in(v__0,v_b,v_x) -> eval_ex3_bb2_in(v__0,v_b,v_x) [-1 + v__0 >= 0 && 254 >= v__0] (?,1) 8. eval_ex3_bb1_in(v__0,v_b,v_x) -> eval_ex3_bb3_in(v__0,v_b,v_x) [0 >= v__0] (?,1) 9. eval_ex3_bb1_in(v__0,v_b,v_x) -> eval_ex3_bb3_in(v__0,v_b,v_x) [v__0 >= 255] (?,1) 10. eval_ex3_bb2_in(v__0,v_b,v_x) -> eval_ex3_bb1_in(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 >= v_b] (?,1) 11. eval_ex3_bb2_in(v__0,v_b,v_x) -> eval_ex3_bb1_in(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 + v_b >= 0] (?,1) 12. eval_ex3_bb2_in(v__0,v_b,v_x) -> eval_ex3_bb1_in(-1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && v_b = 0] (?,1) 13. eval_ex3_bb3_in(v__0,v_b,v_x) -> eval_ex3_stop(v__0,v_b,v_x) True (?,1) Signature: {(eval_ex3_0,3) ;(eval_ex3_1,3) ;(eval_ex3_2,3) ;(eval_ex3_3,3) ;(eval_ex3_4,3) ;(eval_ex3_bb0_in,3) ;(eval_ex3_bb1_in,3) ;(eval_ex3_bb2_in,3) ;(eval_ex3_bb3_in,3) ;(eval_ex3_start,3) ;(eval_ex3_stop,3)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7,8,9},7->{10,11,12},8->{13},9->{13},10->{7,9},11->{7,9} ,12->{7,8},13->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: eval_ex3_start(v__0,v_b,v_x) -> eval_ex3_bb0_in(v__0,v_b,v_x) True eval_ex3_bb0_in(v__0,v_b,v_x) -> eval_ex3_0(v__0,v_b,v_x) True eval_ex3_0(v__0,v_b,v_x) -> eval_ex3_1(v__0,v_b,v_x) True eval_ex3_1(v__0,v_b,v_x) -> eval_ex3_2(v__0,v_b,v_x) True eval_ex3_2(v__0,v_b,v_x) -> eval_ex3_3(v__0,v_b,v_x) True eval_ex3_3(v__0,v_b,v_x) -> eval_ex3_4(v__0,v_b,v_x) True eval_ex3_4(v__0,v_b,v_x) -> eval_ex3_bb1_in(v_x,v_b,v_x) True eval_ex3_bb1_in(v__0,v_b,v_x) -> eval_ex3_bb2_in(v__0,v_b,v_x) [-1 + v__0 >= 0 && 254 >= v__0] eval_ex3_bb1_in(v__0,v_b,v_x) -> eval_ex3_bb3_in(v__0,v_b,v_x) [0 >= v__0] eval_ex3_bb1_in(v__0,v_b,v_x) -> eval_ex3_bb3_in(v__0,v_b,v_x) [v__0 >= 255] eval_ex3_bb2_in(v__0,v_b,v_x) -> eval_ex3_bb1_in(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 >= v_b] eval_ex3_bb2_in(v__0,v_b,v_x) -> eval_ex3_bb1_in(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 + v_b >= 0] eval_ex3_bb2_in(v__0,v_b,v_x) -> eval_ex3_bb1_in(-1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && v_b = 0] eval_ex3_bb3_in(v__0,v_b,v_x) -> eval_ex3_stop(v__0,v_b,v_x) True Signature: {(eval_ex3_0,3) ;(eval_ex3_1,3) ;(eval_ex3_2,3) ;(eval_ex3_3,3) ;(eval_ex3_4,3) ;(eval_ex3_bb0_in,3) ;(eval_ex3_bb1_in,3) ;(eval_ex3_bb2_in,3) ;(eval_ex3_bb3_in,3) ;(eval_ex3_start,3) ;(eval_ex3_stop,3)} Rule Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7,8,9},7->{10,11,12},8->{13},9->{13},10->{7,9},11->{7,9} ,12->{7,8},13->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: eval_ex3_start.0(v__0,v_b,v_x) -> eval_ex3_bb0_in.1(v__0,v_b,v_x) True eval_ex3_bb0_in.1(v__0,v_b,v_x) -> eval_ex3_0.2(v__0,v_b,v_x) True eval_ex3_0.2(v__0,v_b,v_x) -> eval_ex3_1.3(v__0,v_b,v_x) True eval_ex3_1.3(v__0,v_b,v_x) -> eval_ex3_2.4(v__0,v_b,v_x) True eval_ex3_2.4(v__0,v_b,v_x) -> eval_ex3_3.5(v__0,v_b,v_x) True eval_ex3_3.5(v__0,v_b,v_x) -> eval_ex3_4.6(v__0,v_b,v_x) True eval_ex3_4.6(v__0,v_b,v_x) -> eval_ex3_bb1_in.7(v_x,v_b,v_x) True eval_ex3_4.6(v__0,v_b,v_x) -> eval_ex3_bb1_in.8(v_x,v_b,v_x) True eval_ex3_4.6(v__0,v_b,v_x) -> eval_ex3_bb1_in.9(v_x,v_b,v_x) True eval_ex3_bb1_in.7(v__0,v_b,v_x) -> eval_ex3_bb2_in.10(v__0,v_b,v_x) [-1 + v__0 >= 0 && 254 >= v__0] eval_ex3_bb1_in.7(v__0,v_b,v_x) -> eval_ex3_bb2_in.11(v__0,v_b,v_x) [-1 + v__0 >= 0 && 254 >= v__0] eval_ex3_bb1_in.7(v__0,v_b,v_x) -> eval_ex3_bb2_in.12(v__0,v_b,v_x) [-1 + v__0 >= 0 && 254 >= v__0] eval_ex3_bb1_in.8(v__0,v_b,v_x) -> eval_ex3_bb3_in.13(v__0,v_b,v_x) [0 >= v__0] eval_ex3_bb1_in.9(v__0,v_b,v_x) -> eval_ex3_bb3_in.13(v__0,v_b,v_x) [v__0 >= 255] eval_ex3_bb2_in.10(v__0,v_b,v_x) -> eval_ex3_bb1_in.7(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 >= v_b] eval_ex3_bb2_in.10(v__0,v_b,v_x) -> eval_ex3_bb1_in.9(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 >= v_b] eval_ex3_bb2_in.11(v__0,v_b,v_x) -> eval_ex3_bb1_in.7(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 + v_b >= 0] eval_ex3_bb2_in.11(v__0,v_b,v_x) -> eval_ex3_bb1_in.9(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 + v_b >= 0] eval_ex3_bb2_in.12(v__0,v_b,v_x) -> eval_ex3_bb1_in.7(-1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && v_b = 0] eval_ex3_bb2_in.12(v__0,v_b,v_x) -> eval_ex3_bb1_in.8(-1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && v_b = 0] eval_ex3_bb3_in.13(v__0,v_b,v_x) -> eval_ex3_stop.14(v__0,v_b,v_x) True Signature: {(eval_ex3_0.2,3) ;(eval_ex3_1.3,3) ;(eval_ex3_2.4,3) ;(eval_ex3_3.5,3) ;(eval_ex3_4.6,3) ;(eval_ex3_bb0_in.1,3) ;(eval_ex3_bb1_in.7,3) ;(eval_ex3_bb1_in.8,3) ;(eval_ex3_bb1_in.9,3) ;(eval_ex3_bb2_in.10,3) ;(eval_ex3_bb2_in.11,3) ;(eval_ex3_bb2_in.12,3) ;(eval_ex3_bb3_in.13,3) ;(eval_ex3_start.0,3) ;(eval_ex3_stop.14,3)} Rule Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6,7,8},6->{9,10,11},7->{12},8->{13},9->{14,15},10->{16,17},11->{18 ,19},12->{20},13->{20},14->{9,10,11},15->{13},16->{9,10,11},17->{13},18->{9,10,11},19->{12},20->{}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: eval_ex3_start.0(v__0,v_b,v_x) -> eval_ex3_bb0_in.1(v__0,v_b,v_x) True eval_ex3_bb0_in.1(v__0,v_b,v_x) -> eval_ex3_0.2(v__0,v_b,v_x) True eval_ex3_0.2(v__0,v_b,v_x) -> eval_ex3_1.3(v__0,v_b,v_x) True eval_ex3_1.3(v__0,v_b,v_x) -> eval_ex3_2.4(v__0,v_b,v_x) True eval_ex3_2.4(v__0,v_b,v_x) -> eval_ex3_3.5(v__0,v_b,v_x) True eval_ex3_3.5(v__0,v_b,v_x) -> eval_ex3_4.6(v__0,v_b,v_x) True eval_ex3_4.6(v__0,v_b,v_x) -> eval_ex3_bb1_in.7(v_x,v_b,v_x) True eval_ex3_4.6(v__0,v_b,v_x) -> eval_ex3_bb1_in.8(v_x,v_b,v_x) True eval_ex3_4.6(v__0,v_b,v_x) -> eval_ex3_bb1_in.9(v_x,v_b,v_x) True eval_ex3_bb1_in.7(v__0,v_b,v_x) -> eval_ex3_bb2_in.10(v__0,v_b,v_x) [-1 + v__0 >= 0 && 254 >= v__0] eval_ex3_bb1_in.7(v__0,v_b,v_x) -> eval_ex3_bb2_in.11(v__0,v_b,v_x) [-1 + v__0 >= 0 && 254 >= v__0] eval_ex3_bb1_in.7(v__0,v_b,v_x) -> eval_ex3_bb2_in.12(v__0,v_b,v_x) [-1 + v__0 >= 0 && 254 >= v__0] eval_ex3_bb1_in.8(v__0,v_b,v_x) -> eval_ex3_bb3_in.13(v__0,v_b,v_x) [0 >= v__0] eval_ex3_bb1_in.9(v__0,v_b,v_x) -> eval_ex3_bb3_in.13(v__0,v_b,v_x) [v__0 >= 255] eval_ex3_bb2_in.10(v__0,v_b,v_x) -> eval_ex3_bb1_in.7(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 >= v_b] eval_ex3_bb2_in.10(v__0,v_b,v_x) -> eval_ex3_bb1_in.9(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 >= v_b] eval_ex3_bb2_in.11(v__0,v_b,v_x) -> eval_ex3_bb1_in.7(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 + v_b >= 0] eval_ex3_bb2_in.11(v__0,v_b,v_x) -> eval_ex3_bb1_in.9(1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && -1 + v_b >= 0] eval_ex3_bb2_in.12(v__0,v_b,v_x) -> eval_ex3_bb1_in.7(-1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && v_b = 0] eval_ex3_bb2_in.12(v__0,v_b,v_x) -> eval_ex3_bb1_in.8(-1 + v__0,v_b,v_x) [254 + -1*v__0 >= 0 && -1 + v__0 >= 0 && v_b = 0] eval_ex3_bb3_in.13(v__0,v_b,v_x) -> eval_ex3_stop.14(v__0,v_b,v_x) True eval_ex3_stop.14(v__0,v_b,v_x) -> exitus616(v__0,v_b,v_x) True eval_ex3_stop.14(v__0,v_b,v_x) -> exitus616(v__0,v_b,v_x) True eval_ex3_stop.14(v__0,v_b,v_x) -> exitus616(v__0,v_b,v_x) True eval_ex3_stop.14(v__0,v_b,v_x) -> exitus616(v__0,v_b,v_x) True eval_ex3_stop.14(v__0,v_b,v_x) -> exitus616(v__0,v_b,v_x) True Signature: {(eval_ex3_0.2,3) ;(eval_ex3_1.3,3) ;(eval_ex3_2.4,3) ;(eval_ex3_3.5,3) ;(eval_ex3_4.6,3) ;(eval_ex3_bb0_in.1,3) ;(eval_ex3_bb1_in.7,3) ;(eval_ex3_bb1_in.8,3) ;(eval_ex3_bb1_in.9,3) ;(eval_ex3_bb2_in.10,3) ;(eval_ex3_bb2_in.11,3) ;(eval_ex3_bb2_in.12,3) ;(eval_ex3_bb3_in.13,3) ;(eval_ex3_start.0,3) ;(eval_ex3_stop.14,3) ;(exitus616,3)} Rule Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6,7,8},6->{9,10,11},7->{12},8->{13},9->{14,15},10->{16,17},11->{18 ,19},12->{20},13->{20},14->{9,10,11},15->{13},16->{9,10,11},17->{13},18->{9,10,11},19->{12},20->{21,22,23,24 ,25}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25] | `- p:[9,14,16,10,18,11] c: [] MAYBE