- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: ba8971db-09d7-4819-8aa2-530e0cd1b6a4
    creation_time: 2025-03-22T07:20:44Z
    producer:
      name: Goblint
      version: heads/master-0-g66dff5a90-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp.json'' ''--disable'' ''witness.graphml.enabled''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp''
        ''--sets'' ''exp.architecture'' ''64bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i: 51f4cf8ce110b92f68961d27b667e514c3fefcd9540eb44fa919855fdd25ad59
      data_model: LP64
      language: C
      specification: 'CHECK( init(main()), LTL(G valid-free) )

        CHECK( init(main()), LTL(G valid-deref) )

        CHECK( init(main()), LTL(G valid-memtrack) )'
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2939
        column: 3
        function: __main
      value: c <= 0L
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2939
        column: 3
        function: __main
      value: retval == (char)0 || retval == (char)1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2916
        column: 3
        function: __main
      value: retval == (char)0 || retval == (char)1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: -1 == max_arg
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: 0 == min_arg
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: 0 == spec_flgs
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: 0U == flags
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: 0U == requires
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: applet_opts == (char const   *)"ia"
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: flags == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: flags == requires
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: requires == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: min_arg == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: min_arg == spec_flgs
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: max_arg == -1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: spec_flgs == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2434
        column: 3
        function: getopt32
      value: (((5 <= argc || argc == 4) || argc == 3) || argc == 2) || (1 == argc
        && argc == 1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: 0 <= c
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: 1 <= argc
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: c <= 32
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: -1 == max_arg
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: 0 == min_arg
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: 0 == spec_flgs
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: 0U == flags
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: 0U == requires
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: flags == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: flags == requires
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: requires == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: s == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: min_arg == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: min_arg == spec_flgs
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: max_arg == -1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2537
        column: 3
        function: getopt32
      value: spec_flgs == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 3128
        column: 3
        function: main
      value: (((((((((i == 10 || i == 9) || i == 8) || i == 7) || i == 6) || i ==
        5) || i == 4) || i == 3) || i == 2) || i == 1) || (0 == i && i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2775
        column: 3
        function: getopt32
      value: 1 <= argc
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2775
        column: 3
        function: getopt32
      value: requires == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2775
        column: 3
        function: getopt32
      value: c == -1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2775
        column: 3
        function: getopt32
      value: s == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2775
        column: 3
        function: getopt32
      value: min_arg == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2775
        column: 3
        function: getopt32
      value: max_arg == -1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2775
        column: 3
        function: getopt32
      value: spec_flgs == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2775
        column: 3
        function: getopt32
      value: tmp_if_expr$7 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2746
        column: 5
        function: getopt32
      value: 1 <= argc
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2746
        column: 5
        function: getopt32
      value: requires == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2746
        column: 5
        function: getopt32
      value: s == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2746
        column: 5
        function: getopt32
      value: min_arg == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2746
        column: 5
        function: getopt32
      value: max_arg == -1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2746
        column: 5
        function: getopt32
      value: spec_flgs == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2746
        column: 5
        function: getopt32
      value: tmp_if_expr$7 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: 1 <= argc
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: -1 == max_arg
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: 0 == min_arg
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: 0 == spec_flgs
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: 0U == flags
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: 0U == requires
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: flags == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: flags == requires
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: requires == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: min_arg == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: min_arg == spec_flgs
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: max_arg == -1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: spec_flgs == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2461
        column: 7
        function: getopt32
      value: ((((((((((((((((((((4 <= c && c <= 31) || (c == 3 && on_off == & complementary[3]))
        || (c == 3 && on_off == & complementary[3])) || (c == 3 && on_off == & complementary[3]))
        || (c == 3 && on_off == & complementary[3])) || (c == 3 && on_off == & complementary[3]))
        || (c == 2 && on_off == & complementary[2])) || (c == 2 && on_off == & complementary[2]))
        || (c == 2 && on_off == & complementary[2])) || (c == 2 && on_off == & complementary[2]))
        || (c == 2 && on_off == & complementary[2])) || (c == 1 && on_off == & complementary[1]))
        || (c == 1 && on_off == & complementary[1])) || (c == 1 && on_off == & complementary[1]))
        || (c == 1 && on_off == & complementary[1])) || (c == 1 && on_off == & complementary[1]))
        || (((((0 == c && c == 0) && c == min_arg) && c == spec_flgs) && on_off ==
        & complementary[0]) && on_off == complementary)) || (((((0 == c && c == 0)
        && c == min_arg) && c == spec_flgs) && on_off == & complementary[0]) && on_off
        == complementary)) || (((((0 == c && c == 0) && c == min_arg) && c == spec_flgs)
        && on_off == & complementary[0]) && on_off == complementary)) || (((((0 ==
        c && c == 0) && c == min_arg) && c == spec_flgs) && on_off == & complementary[0])
        && on_off == complementary)) || (((((0 == c && c == 0) && c == min_arg) &&
        c == spec_flgs) && on_off == & complementary[0]) && on_off == complementary)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2844
        column: 3
        function: safe_write
      value: 1UL <= count
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2844
        column: 3
        function: safe_write
      value: 2 == fd
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2844
        column: 3
        function: safe_write
      value: fd == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2739
        column: 3
        function: getopt32
      value: 0 <= c
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2739
        column: 3
        function: getopt32
      value: 1 <= argc
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2739
        column: 3
        function: getopt32
      value: requires == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2739
        column: 3
        function: getopt32
      value: s == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2739
        column: 3
        function: getopt32
      value: min_arg == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2739
        column: 3
        function: getopt32
      value: max_arg == -1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2739
        column: 3
        function: getopt32
      value: spec_flgs == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2739
        column: 3
        function: getopt32
      value: tmp_if_expr$7 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2739
        column: 3
        function: getopt32
      value: (c <= 255 || (((((((((c <= 32 && -1 == max_arg) && (_Bool)0 == tmp_if_expr$7)
        && 0 == min_arg) && 0 == spec_flgs) && 0U == flags) && 0U == requires) &&
        flags == 0U) && flags == requires) && min_arg == spec_flgs)) || c <= 255
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2829
        column: 3
        function: safe_read
      value: 0 == fd
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2829
        column: 3
        function: safe_read
      value: fd == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2829
        column: 3
        function: safe_read
      value: count == 8193UL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 3143
        column: 5
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 3143
        column: 5
        function: main
      value: (((((((((((((((((((((((((((((((((((((((((((((((((((9 <= i && 10 <= argc)
        && i <= 2147483646) || (9 <= argc && i == 8)) || (8 <= argc && i == 7)) ||
        (7 <= argc && i == 6)) || (6 <= argc && i == 5)) || (5 <= argc && i == 4))
        && ((((((((((j == 10 || j == 9) || j == 8) || j == 7) || j == 6) || j == 5)
        || j == 4) || j == 3) || j == 2) || j == 1) || (0 == j && j == 0))) || ((4
        <= argc && i == 3) && j == 10)) || ((4 <= argc && i == 3) && j == 9)) || ((4
        <= argc && i == 3) && j == 8)) || ((4 <= argc && i == 3) && j == 7)) || ((4
        <= argc && i == 3) && j == 6)) || ((4 <= argc && i == 3) && j == 5)) || ((4
        <= argc && i == 3) && j == 4)) || ((4 <= argc && i == 3) && j == 3)) || ((4
        <= argc && i == 3) && j == 2)) || ((4 <= argc && i == 3) && j == 1)) || (((4
        <= argc && 0 == j) && i == 3) && j == 0)) || ((3 <= argc && i == 2) && j ==
        10)) || ((3 <= argc && i == 2) && j == 9)) || ((3 <= argc && i == 2) && j
        == 8)) || ((3 <= argc && i == 2) && j == 7)) || ((3 <= argc && i == 2) &&
        j == 6)) || ((3 <= argc && i == 2) && j == 5)) || ((3 <= argc && i == 2) &&
        j == 4)) || ((3 <= argc && i == 2) && j == 3)) || ((3 <= argc && i == 2) &&
        j == 2)) || ((3 <= argc && i == 2) && j == 1)) || (((3 <= argc && 0 == j)
        && i == 2) && j == 0)) || ((2 <= argc && i == 1) && j == 10)) || ((2 <= argc
        && i == 1) && j == 9)) || ((2 <= argc && i == 1) && j == 8)) || ((2 <= argc
        && i == 1) && j == 7)) || ((2 <= argc && i == 1) && j == 6)) || ((2 <= argc
        && i == 1) && j == 5)) || ((2 <= argc && i == 1) && j == 4)) || ((2 <= argc
        && i == 1) && j == 3)) || ((2 <= argc && i == 1) && j == 2)) || ((2 <= argc
        && i == 1) && j == 1)) || (((2 <= argc && 0 == j) && i == 1) && j == 0)) ||
        ((1 <= argc && i == 0) && j == 10)) || ((1 <= argc && i == 0) && j == 9))
        || ((1 <= argc && i == 0) && j == 8)) || ((1 <= argc && i == 0) && j == 7))
        || ((1 <= argc && i == 0) && j == 6)) || ((1 <= argc && i == 0) && j == 5))
        || ((1 <= argc && i == 0) && j == 4)) || ((1 <= argc && i == 0) && j == 3))
        || ((1 <= argc && i == 0) && j == 2)) || ((1 <= argc && i == 0) && j == 1))
        || (((1 <= argc && 0 == j) && i == 0) && j == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 3147
        column: 3
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 3147
        column: 3
        function: main
      value: res == 0 || res == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 3147
        column: 3
        function: main
      value: (j == 10 && ((((((((((((((((((((((((((((((((((((4 <= i && (((((((((((((((((((((((((((((((((((((((((10
        <= argc && 10 <= i) || ((i <= 9 && argc == 9) && i == 9)) || ((i <= 8 && argc
        == 8) && i == 8)) || ((i <= 9 && argc == 9) && i == 9)) || ((i <= 8 && argc
        == 8) && i == 8)) || ((i <= 7 && argc == 7) && i == 7)) || ((i <= 7 && argc
        == 7) && i == 7)) || ((i <= 6 && argc == 6) && i == 6)) || ((i <= 6 && argc
        == 6) && i == 6)) || ((i <= 5 && argc == 5) && i == 5)) || ((i <= 5 && argc
        == 5) && i == 5)) || ((i <= 9 && argc == 9) && i == 9)) || ((i <= 8 && argc
        == 8) && i == 8)) || ((i <= 9 && argc == 9) && i == 9)) || ((i <= 8 && argc
        == 8) && i == 8)) || ((i <= 9 && argc == 9) && i == 9)) || ((i <= 8 && argc
        == 8) && i == 8)) || ((i <= 9 && argc == 9) && i == 9)) || ((i <= 8 && argc
        == 8) && i == 8)) || ((i <= 9 && argc == 9) && i == 9)) || ((i <= 8 && argc
        == 8) && i == 8)) || ((i <= 9 && argc == 9) && i == 9)) || ((i <= 8 && argc
        == 8) && i == 8)) || ((i <= 7 && argc == 7) && i == 7)) || ((i <= 7 && argc
        == 7) && i == 7)) || ((i <= 7 && argc == 7) && i == 7)) || ((i <= 7 && argc
        == 7) && i == 7)) || ((i <= 7 && argc == 7) && i == 7)) || ((i <= 7 && argc
        == 7) && i == 7)) || ((i <= 6 && argc == 6) && i == 6)) || ((i <= 6 && argc
        == 6) && i == 6)) || ((i <= 6 && argc == 6) && i == 6)) || ((i <= 6 && argc
        == 6) && i == 6)) || ((i <= 6 && argc == 6) && i == 6)) || ((i <= 6 && argc
        == 6) && i == 6)) || ((i <= 5 && argc == 5) && i == 5)) || ((i <= 5 && argc
        == 5) && i == 5)) || ((i <= 5 && argc == 5) && i == 5)) || ((i <= 5 && argc
        == 5) && i == 5)) || ((i <= 5 && argc == 5) && i == 5)) || ((i <= 5 && argc
        == 5) && i == 5))) || ((argc == 4 && i == 4) && i == 4)) || ((argc == 4 &&
        i == 4) && i == 4)) || ((argc == 4 && i == 4) && i == 4)) || ((argc == 4 &&
        i == 4) && i == 4)) || ((argc == 4 && i == 4) && i == 4)) || ((argc == 4 &&
        i == 4) && i == 4)) || ((argc == 4 && i == 4) && i == 4)) || ((argc == 4 &&
        i == 4) && i == 4)) || (((4 <= i && i <= 9) && argc == 9) && i == 9)) || (((4
        <= i && i <= 8) && argc == 8) && i == 8)) || (((4 <= i && i <= 9) && argc
        == 9) && i == 9)) || (((4 <= i && i <= 8) && argc == 8) && i == 8)) || (((4
        <= i && i <= 9) && argc == 9) && i == 9)) || (((4 <= i && i <= 8) && argc
        == 8) && i == 8)) || (((4 <= i && i <= 9) && argc == 9) && i == 9)) || (((4
        <= i && i <= 8) && argc == 8) && i == 8)) || (((4 <= i && i <= 7) && argc
        == 7) && i == 7)) || (((4 <= i && i <= 7) && argc == 7) && i == 7)) || (((4
        <= i && i <= 7) && argc == 7) && i == 7)) || (((4 <= i && i <= 7) && argc
        == 7) && i == 7)) || (((4 <= i && i <= 6) && argc == 6) && i == 6)) || (((4
        <= i && i <= 6) && argc == 6) && i == 6)) || (((4 <= i && i <= 5) && argc
        == 5) && i == 5)) || (((4 <= i && i <= 5) && argc == 5) && i == 5)) || (((4
        <= i && i <= 6) && argc == 6) && i == 6)) || (((4 <= i && i <= 6) && argc
        == 6) && i == 6)) || (((4 <= i && i <= 5) && argc == 5) && i == 5)) || (((4
        <= i && i <= 5) && argc == 5) && i == 5)) || ((argc == 4 && i == 4) && i ==
        4)) || ((argc == 4 && i == 4) && i == 4)) || ((argc == 4 && i == 4) && i ==
        4)) || ((argc == 4 && i == 4) && i == 4)) || (i == 3 && (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= argc && 10 <= i) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) ||
        (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 7 && i == 7))
        || (argc == 7 && i == 7)) || (argc == 6 && i == 6)) || (argc == 6 && i ==
        6)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 9 && i
        == 9)) || (argc == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc == 8 &&
        i == 8)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 9
        && i == 9)) || (argc == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc ==
        8 && i == 8)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc
        == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc
        == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc
        == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc
        == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc
        == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc
        == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc
        == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc == 3 && i == 3)) || (argc
        == 3 && i == 3)) || (argc == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc
        == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc
        == 4 && i == 4)) || (argc == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc
        == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc
        == 3 && i == 3)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc
        == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc
        == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc
        == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc
        == 7 && i == 7)) || (argc == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc
        == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 6 && i == 6)) || (argc
        == 6 && i == 6)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc
        == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc == 3 && i == 3)) || (argc
        == 3 && i == 3)) || (argc == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc
        == 3 && i == 3)) || (argc == 3 && i == 3)))) || (i == 2 && (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= argc && 10 <= i) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) ||
        (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 7 && i == 7))
        || (argc == 7 && i == 7)) || (argc == 6 && i == 6)) || (argc == 6 && i ==
        6)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 9 && i
        == 9)) || (argc == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc == 8 &&
        i == 8)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 9
        && i == 9)) || (argc == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc ==
        8 && i == 8)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc
        == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc
        == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc
        == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc
        == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc
        == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc
        == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc
        == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc == 3 && i == 3)) || (argc
        == 3 && i == 3)) || (argc == 2 && i == 2)) || (argc == 2 && i == 2)) || (argc
        == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc
        == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc
        == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc
        == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc
        == 2 && i == 2)) || (argc == 2 && i == 2)) || (argc == 2 && i == 2)) || (argc
        == 2 && i == 2)) || (argc == 2 && i == 2)) || (argc == 2 && i == 2)) || (argc
        == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc
        == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc
        == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 7 && i == 7)) || (argc
        == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc
        == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc == 5 && i == 5)) || (argc
        == 5 && i == 5)) || (argc == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc
        == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 4 && i == 4)) || (argc
        == 4 && i == 4)) || (argc == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc
        == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc == 3 && i == 3)) || (argc
        == 3 && i == 3)) || (argc == 2 && i == 2)) || (argc == 2 && i == 2)) || (argc
        == 2 && i == 2)) || (argc == 2 && i == 2)))) || (i == 1 && (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= argc && 10 <= i) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) ||
        (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 7 && i == 7))
        || (argc == 7 && i == 7)) || (argc == 6 && i == 6)) || (argc == 6 && i ==
        6)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 9 && i
        == 9)) || (argc == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc == 8 &&
        i == 8)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 9
        && i == 9)) || (argc == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc ==
        8 && i == 8)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc
        == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc
        == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc
        == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc
        == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc
        == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc
        == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc
        == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc == 3 && i == 3)) || (argc
        == 3 && i == 3)) || (argc == 2 && i == 2)) || (argc == 1 && i == 1)) || (argc
        == 2 && i == 2)) || (argc == 1 && i == 1)) || (argc == 4 && i == 4)) || (argc
        == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc
        == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc == 3 && i == 3)) || (argc
        == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc
        == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc == 2 && i == 2)) || (argc
        == 1 && i == 1)) || (argc == 2 && i == 2)) || (argc == 1 && i == 1)) || (argc
        == 2 && i == 2)) || (argc == 1 && i == 1)) || (argc == 2 && i == 2)) || (argc
        == 1 && i == 1)) || (argc == 2 && i == 2)) || (argc == 1 && i == 1)) || (argc
        == 2 && i == 2)) || (argc == 1 && i == 1)) || (argc == 9 && i == 9)) || (argc
        == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc
        == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc
        == 8 && i == 8)) || (argc == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc
        == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc == 6 && i == 6)) || (argc
        == 6 && i == 6)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc
        == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc == 5 && i == 5)) || (argc
        == 5 && i == 5)) || (argc == 4 && i == 4)) || (argc == 4 && i == 4)) || (argc
        == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc == 4 && i == 4)) || (argc
        == 4 && i == 4)) || (argc == 3 && i == 3)) || (argc == 3 && i == 3)) || (argc
        == 2 && i == 2)) || (argc == 1 && i == 1)) || (argc == 2 && i == 2)) || (argc
        == 1 && i == 1)) || (argc == 2 && i == 2)) || (argc == 1 && i == 1)) || (argc
        == 2 && i == 2)) || (argc == 1 && i == 1))))) || ((0 == i && i == 0) && (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((j
        == 10 && (((((((((((((((((((((((((((((((((((((((((((((10 <= argc && 10 <=
        i) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 9 && i
        == 9)) || (argc == 8 && i == 8)) || (argc == 7 && i == 7)) || (argc == 7 &&
        i == 7)) || (argc == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc == 5
        && i == 5)) || (argc == 5 && i == 5)) || (argc == 9 && i == 9)) || (argc ==
        8 && i == 8)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc
        == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc
        == 8 && i == 8)) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc
        == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 7 && i == 7)) || (argc
        == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc
        == 7 && i == 7)) || (argc == 7 && i == 7)) || (argc == 6 && i == 6)) || (argc
        == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc
        == 6 && i == 6)) || (argc == 6 && i == 6)) || (argc == 5 && i == 5)) || (argc
        == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc
        == 5 && i == 5)) || (argc == 5 && i == 5)) || (argc == 4 && i == 4)) || (argc
        == 4 && i == 4)) || (argc == 3 && i == 3)) || (argc == 3 && i == 3))) || (argc
        <= 0 && i == 0)) || ((argc == 2 && i == 2) && j == 10)) || ((argc == 1 &&
        i == 1) && j == 10)) || (argc <= 0 && i == 0)) || ((argc == 2 && i == 2) &&
        j == 10)) || ((argc == 1 && i == 1) && j == 10)) || ((argc == 4 && i == 4)
        && j == 10)) || ((argc == 4 && i == 4) && j == 10)) || ((argc == 4 && i ==
        4) && j == 10)) || ((argc == 4 && i == 4) && j == 10)) || ((argc == 4 && i
        == 4) && j == 10)) || ((argc == 4 && i == 4) && j == 10)) || ((argc == 3 &&
        i == 3) && j == 10)) || ((argc == 3 && i == 3) && j == 10)) || ((argc == 3
        && i == 3) && j == 10)) || ((argc == 3 && i == 3) && j == 10)) || ((argc ==
        3 && i == 3) && j == 10)) || ((argc == 3 && i == 3) && j == 10)) || (argc
        <= 0 && i == 0)) || ((argc == 2 && i == 2) && j == 10)) || ((argc == 1 &&
        i == 1) && j == 10)) || (argc <= 0 && i == 0)) || ((argc == 2 && i == 2) &&
        j == 10)) || ((argc == 1 && i == 1) && j == 10)) || (argc <= 0 && i == 0))
        || ((argc == 2 && i == 2) && j == 10)) || ((argc == 1 && i == 1) && j == 10))
        || (argc <= 0 && i == 0)) || ((argc == 2 && i == 2) && j == 10)) || ((argc
        == 1 && i == 1) && j == 10)) || (argc <= 0 && i == 0)) || ((argc == 2 && i
        == 2) && j == 10)) || ((argc == 1 && i == 1) && j == 10)) || (argc <= 0 &&
        i == 0)) || ((argc == 2 && i == 2) && j == 10)) || ((argc == 1 && i == 1)
        && j == 10)) || ((argc == 9 && i == 9) && j == 10)) || ((argc == 8 && i ==
        8) && j == 10)) || ((argc == 9 && i == 9) && j == 10)) || ((argc == 8 && i
        == 8) && j == 10)) || ((argc == 9 && i == 9) && j == 10)) || ((argc == 8 &&
        i == 8) && j == 10)) || ((argc == 9 && i == 9) && j == 10)) || ((argc == 8
        && i == 8) && j == 10)) || ((argc == 7 && i == 7) && j == 10)) || ((argc ==
        7 && i == 7) && j == 10)) || ((argc == 7 && i == 7) && j == 10)) || ((argc
        == 7 && i == 7) && j == 10)) || ((argc == 6 && i == 6) && j == 10)) || ((argc
        == 6 && i == 6) && j == 10)) || ((argc == 5 && i == 5) && j == 10)) || ((argc
        == 5 && i == 5) && j == 10)) || ((argc == 6 && i == 6) && j == 10)) || ((argc
        == 6 && i == 6) && j == 10)) || ((argc == 5 && i == 5) && j == 10)) || ((argc
        == 5 && i == 5) && j == 10)) || ((argc == 4 && i == 4) && j == 10)) || ((argc
        == 4 && i == 4) && j == 10)) || ((argc == 3 && i == 3) && j == 10)) || ((argc
        == 3 && i == 3) && j == 10)) || ((argc == 4 && i == 4) && j == 10)) || ((argc
        == 4 && i == 4) && j == 10)) || ((argc == 3 && i == 3) && j == 10)) || ((argc
        == 3 && i == 3) && j == 10)) || (argc <= 0 && i == 0)) || ((argc == 2 && i
        == 2) && j == 10)) || ((argc == 1 && i == 1) && j == 10)) || (argc <= 0 &&
        i == 0)) || ((argc == 2 && i == 2) && j == 10)) || ((argc == 1 && i == 1)
        && j == 10)) || (argc <= 0 && i == 0)) || ((argc == 2 && i == 2) && j == 10))
        || ((argc == 1 && i == 1) && j == 10)) || (argc <= 0 && i == 0)) || ((argc
        == 2 && i == 2) && j == 10)) || ((argc == 1 && i == 1) && j == 10)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2922
        column: 5
        function: __main
      value: 1L <= c
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2922
        column: 5
        function: __main
      value: retval == (char)0 || retval == (char)1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 3138
        column: 3
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 3138
        column: 3
        function: main
      value: (j == 10 && ((((((((((10 <= argc && 10 <= i) || (9 <= argc && i == 9))
        || (8 <= argc && i == 8)) || (7 <= argc && i == 7)) || (6 <= argc && i ==
        6)) || (5 <= argc && i == 5)) || (4 <= argc && i == 4)) || (3 <= argc && i
        == 3)) || (2 <= argc && i == 2)) || (1 <= argc && i == 1))) || (0 == i &&
        i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2401
        column: 3
        function: full_write
      value: 2 == fd
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2401
        column: 3
        function: full_write
      value: fd == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2401
        column: 3
        function: full_write
      value: (0L <= cc && 0L <= total) || (0L == total && total == 0L)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: 1 <= argc
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: -1 == max_arg
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: 0 == min_arg
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: 0 == spec_flgs
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: 0U == flags
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: 0U == requires
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: flags == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: flags == requires
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: requires == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: min_arg == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: min_arg == spec_flgs
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: max_arg == -1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: spec_flgs == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/tee-2.i
        line: 2451
        column: 3
        function: getopt32
      value: ((((4 <= c && c <= 32) || (c == 3 && on_off == & complementary[3])) ||
        (c == 2 && on_off == & complementary[2])) || (c == 1 && on_off == & complementary[1]))
        || (((((0 == c && c == 0) && c == min_arg) && c == spec_flgs) && on_off ==
        & complementary[0]) && on_off == complementary)
      format: c_expression
