Function foo

    line 341
    max(call_to_nondet_line_32, call_to_nondet_line_142, call_to_nondet_line_253, 0)
    O(n)
    line 376
    FAILED to compute RF
      line 371
      FAILED to compute RF
        line 371
        FAILED to compute RF
          line 516
          FAILED to compute RF
    line 591
    FAILED to compute RF
    line 764
    FAILED to compute RF