Function foo

    line 76
    max(call_to_nondet_line_390, 0)
    O(n)
    line 361
    max(call_to_nondet_line_327, 0)
    O(n)
    line 289
    max(call_to_nondet_line_43, call_to_nondet_line_12, 0)
    O(n)
    line 114
    max(call_to_nondet_line_79, 0)
    O(n)
    line 215
    max(call_to_nondet_line_117, 0)
    O(n)
    line 271
    FAILED to compute RF