Function foo

    line 56
    FAILED to compute RF
    line 405
    FAILED to compute RF
    line 327
    FAILED to compute RF
    line 100
    FAILED to compute RF
    line 277
    max(call_to_nondet_line_103, 0)
    O(n)
    line 309
    FAILED to compute RF