Function foo

    line 253
    max(call_to_nondet_line_737, 0)
    O(n)
    line 288
    1 + max(P1, 0)
    O(n)
      line 283
      FAILED to compute RF
        line 283
        FAILED to compute RF
    line 713
    FAILED to compute RF