Function foo

    line 183
    max(call_to_nondet_line_171, 0)
    O(n)
    line 306
    FAILED to compute RF
    line 809
    FAILED to compute RF