MAYBE
* Step 1: TrivialSCCs 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)  [-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)  [-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) [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:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: AddSinks 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,1)
          2.  eval_ex3_0(v__0,v_b,v_x)      -> eval_ex3_1(v__0,v_b,v_x)           True                            (1,1)
          3.  eval_ex3_1(v__0,v_b,v_x)      -> eval_ex3_2(v__0,v_b,v_x)           True                            (1,1)
          4.  eval_ex3_2(v__0,v_b,v_x)      -> eval_ex3_3(v__0,v_b,v_x)           True                            (1,1)
          5.  eval_ex3_3(v__0,v_b,v_x)      -> eval_ex3_4(v__0,v_b,v_x)           True                            (1,1)
          6.  eval_ex3_4(v__0,v_b,v_x)      -> eval_ex3_bb1_in(v_x,v_b,v_x)       True                            (1,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,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,1)
          10. eval_ex3_bb2_in(v__0,v_b,v_x) -> eval_ex3_bb1_in(1 + v__0,v_b,v_x)  [-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)  [-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) [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,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:
        AddSinks
    + Details:
        ()
* Step 3: Failure 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)  [-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)  [-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) [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)
        14. eval_ex3_bb3_in(v__0,v_b,v_x) -> exitus616(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)
        ;(exitus616,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,14},9->{13,14},10->{7,8,9}
        ,11->{7,8,9},12->{7,8,9},13->{},14->{}]
      
  + Applied Processor:
      LooptreeTransformer
  + Details:
      We construct a looptree:
        P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
        |
        `- p:[7,10,11,12] c: []
MAYBE