Function foo

    line 25
    max(call_to_nondet_line_9, 0)
    O(n)
    line 43
    FAILED to compute RF
    line 67
    FAILED to compute RF
    line 88
    FAILED to compute RF