Function foo

    line 150
    max(0, (call_to_nondet_line_16 + -2))
    O(n)
    line 239
    FAILED to compute RF
    line 281
    FAILED to compute RF