- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 663cfa65-0429-4e6e-b13c-7e0812bc587c
    creation_time: 2025-03-21T02:23:53Z
    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/goblint-coreutils/instrumented_interval_cksum_comb.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i: c92169288ba10e606aecd7ff04f59d0eb48b56f4c981fd9086bac53fae53e7ad
      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/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: -128 <= d->rpl_optopt
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: -1 <= indfound
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: d->rpl_optopt <= 127
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: argc == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: longind == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: longind == (int *)((void *)0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: long_only == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: posixly_correct == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: d->__initialized == 0 || d->__initialized == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: d->__posixly_correct == 0 || d->__posixly_correct == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: ((ambig_list == pn && exact == 1) && ((((((((((((((((((((((((((2 <= option_index
        || 3 <= option_index) || 9 <= option_index) || 9 <= option_index) || 9 <=
        option_index) || 10 <= option_index) || 10 <= option_index) || 9 <= option_index)
        || 10 <= option_index) || 10 <= option_index) || 5 <= option_index) || 5 <=
        option_index) || 4 <= option_index) || 9 <= option_index) || 9 <= option_index)
        || 9 <= option_index) || 10 <= option_index) || 10 <= option_index) || 9 <=
        option_index) || 10 <= option_index) || 10 <= option_index) || 5 <= option_index)
        || 5 <= option_index) || 4 <= option_index) || (((((((((((((((((((((((((((((((2
        <= option_index || 3 <= option_index) || 8 <= option_index) || 8 <= option_index)
        || 8 <= option_index) || 10 <= option_index) || 9 <= option_index) || 10 <=
        option_index) || 9 <= option_index) || 8 <= option_index) || 10 <= option_index)
        || 9 <= option_index) || 10 <= option_index) || 9 <= option_index) || 5 <=
        option_index) || 5 <= option_index) || 4 <= option_index) || 8 <= option_index)
        || 8 <= option_index) || 8 <= option_index) || 10 <= option_index) || 9 <=
        option_index) || 10 <= option_index) || 9 <= option_index) || 8 <= option_index)
        || 10 <= option_index) || 9 <= option_index) || 10 <= option_index) || 9 <=
        option_index) || 5 <= option_index) || 5 <= option_index) || 4 <= option_index))
        || (((((((((((((((((((((((((((((((((((((((2 <= option_index || 3 <= option_index)
        || 7 <= option_index) || 7 <= option_index) || 7 <= option_index) || 9 <=
        option_index) || 10 <= option_index) || 8 <= option_index) || 9 <= option_index)
        || 10 <= option_index) || 8 <= option_index) || 7 <= option_index) || 9 <=
        option_index) || 10 <= option_index) || 8 <= option_index) || 9 <= option_index)
        || 10 <= option_index) || 8 <= option_index) || 5 <= option_index) || 5 <=
        option_index) || 4 <= option_index) || 7 <= option_index) || 7 <= option_index)
        || 7 <= option_index) || 9 <= option_index) || 10 <= option_index) || 8 <=
        option_index) || 9 <= option_index) || 10 <= option_index) || 8 <= option_index)
        || 7 <= option_index) || 9 <= option_index) || 10 <= option_index) || 8 <=
        option_index) || 9 <= option_index) || 10 <= option_index) || 8 <= option_index)
        || 5 <= option_index) || 5 <= option_index) || 4 <= option_index)) || (((((((((((((((((((((((((((((((((((((((((((((((2
        <= option_index || 3 <= option_index) || 6 <= option_index) || 6 <= option_index)
        || 6 <= option_index) || 8 <= option_index) || 10 <= option_index) || 9 <=
        option_index) || 7 <= option_index) || 8 <= option_index) || 10 <= option_index)
        || 9 <= option_index) || 7 <= option_index) || 6 <= option_index) || 8 <=
        option_index) || 10 <= option_index) || 9 <= option_index) || 7 <= option_index)
        || 8 <= option_index) || 10 <= option_index) || 9 <= option_index) || 7 <=
        option_index) || 5 <= option_index) || 5 <= option_index) || 4 <= option_index)
        || 6 <= option_index) || 6 <= option_index) || 6 <= option_index) || 8 <=
        option_index) || 10 <= option_index) || 9 <= option_index) || 7 <= option_index)
        || 8 <= option_index) || 10 <= option_index) || 9 <= option_index) || 7 <=
        option_index) || 6 <= option_index) || 8 <= option_index) || 10 <= option_index)
        || 9 <= option_index) || 7 <= option_index) || 8 <= option_index) || 10 <=
        option_index) || 9 <= option_index) || 7 <= option_index) || 5 <= option_index)
        || 5 <= option_index) || 4 <= option_index))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= option_index && ambig_list == 0) && (exact == 0 || exact == 1)) || ((2
        <= option_index && ambig_list == newp) && exact == 1)) || ((5 <= option_index
        && ambig_list == newp) && exact == 1)) || ((5 <= option_index && ambig_list
        == newp) && exact == 1)) || ((5 <= option_index && ambig_list == newp) &&
        exact == 1)) || ((7 <= option_index && ambig_list == newp) && exact == 1))
        || ((10 <= option_index && ambig_list == newp) && exact == 1)) || ((8 <= option_index
        && ambig_list == newp) && exact == 1)) || ((9 <= option_index && ambig_list
        == newp) && exact == 1)) || ((6 <= option_index && ambig_list == newp) &&
        exact == 1)) || ((7 <= option_index && ambig_list == newp) && exact == 1))
        || ((10 <= option_index && ambig_list == newp) && exact == 1)) || ((8 <= option_index
        && ambig_list == newp) && exact == 1)) || ((9 <= option_index && ambig_list
        == newp) && exact == 1)) || ((6 <= option_index && ambig_list == newp) &&
        exact == 1)) || ((5 <= option_index && ambig_list == newp) && exact == 1))
        || ((7 <= option_index && ambig_list == newp) && exact == 1)) || ((10 <= option_index
        && ambig_list == newp) && exact == 1)) || ((8 <= option_index && ambig_list
        == newp) && exact == 1)) || ((9 <= option_index && ambig_list == newp) &&
        exact == 1)) || ((6 <= option_index && ambig_list == newp) && exact == 1))
        || ((7 <= option_index && ambig_list == newp) && exact == 1)) || ((10 <= option_index
        && ambig_list == newp) && exact == 1)) || ((8 <= option_index && ambig_list
        == newp) && exact == 1)) || ((9 <= option_index && ambig_list == newp) &&
        exact == 1)) || ((6 <= option_index && ambig_list == newp) && exact == 1))
        || ((4 <= option_index && ambig_list == newp) && exact == 1)) || ((4 <= option_index
        && ambig_list == newp) && exact == 1)) || ((3 <= option_index && ambig_list
        == newp) && exact == 1)) || ((5 <= option_index && ambig_list == newp) &&
        exact == 1)) || ((5 <= option_index && ambig_list == newp) && exact == 1))
        || ((5 <= option_index && ambig_list == newp) && exact == 1)) || ((7 <= option_index
        && ambig_list == newp) && exact == 1)) || ((10 <= option_index && ambig_list
        == newp) && exact == 1)) || ((8 <= option_index && ambig_list == newp) &&
        exact == 1)) || ((9 <= option_index && ambig_list == newp) && exact == 1))
        || ((6 <= option_index && ambig_list == newp) && exact == 1)) || ((7 <= option_index
        && ambig_list == newp) && exact == 1)) || ((10 <= option_index && ambig_list
        == newp) && exact == 1)) || ((8 <= option_index && ambig_list == newp) &&
        exact == 1)) || ((9 <= option_index && ambig_list == newp) && exact == 1))
        || ((6 <= option_index && ambig_list == newp) && exact == 1)) || ((5 <= option_index
        && ambig_list == newp) && exact == 1)) || ((7 <= option_index && ambig_list
        == newp) && exact == 1)) || ((10 <= option_index && ambig_list == newp) &&
        exact == 1)) || ((8 <= option_index && ambig_list == newp) && exact == 1))
        || ((9 <= option_index && ambig_list == newp) && exact == 1)) || ((6 <= option_index
        && ambig_list == newp) && exact == 1)) || ((7 <= option_index && ambig_list
        == newp) && exact == 1)) || ((10 <= option_index && ambig_list == newp) &&
        exact == 1)) || ((8 <= option_index && ambig_list == newp) && exact == 1))
        || ((9 <= option_index && ambig_list == newp) && exact == 1)) || ((6 <= option_index
        && ambig_list == newp) && exact == 1)) || ((4 <= option_index && ambig_list
        == newp) && exact == 1)) || ((4 <= option_index && ambig_list == newp) &&
        exact == 1)) || ((3 <= option_index && ambig_list == newp) && exact == 1))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73614
        column: 13
        function: _getopt_internal_r
      value: ((unsigned int )d->__ordering == 0U || (unsigned int )d->__ordering ==
        1U) || (unsigned int )d->__ordering == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72149
        column: 7
        function: exchange
      value: -2147483647 <= middle
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72149
        column: 7
        function: exchange
      value: -128 <= d->rpl_optopt
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72149
        column: 7
        function: exchange
      value: bottom <= 2147483645
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72149
        column: 7
        function: exchange
      value: middle <= 2147483646
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72149
        column: 7
        function: exchange
      value: d->rpl_optopt <= 127
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72149
        column: 7
        function: exchange
      value: d->__initialized == 0 || d->__initialized == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72149
        column: 7
        function: exchange
      value: d->__posixly_correct == 0 || d->__posixly_correct == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72149
        column: 7
        function: exchange
      value: ((unsigned int )d->__ordering == 0U || (unsigned int )d->__ordering ==
        1U) || (unsigned int )d->__ordering == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72149
        column: 7
        function: exchange
      value: (((((-2147483646 <= top && ((((((((((((((((((((4 <= len___0 && 4 <= i___0)
        || (3 <= len___0 && i___0 == 3)) || (2 <= len___0 && i___0 == 2)) || (1 <=
        len___0 && i___0 == 1)) || (0 == i___0 && i___0 == 0)) || (4 <= len___0 &&
        4 <= i___0)) || (3 <= len___0 && i___0 == 3)) || (2 <= len___0 && i___0 ==
        2)) || (1 <= len___0 && i___0 == 1)) || (0 == i___0 && i___0 == 0)) || (4
        <= len___0 && 4 <= i___0)) || (3 <= len___0 && i___0 == 3)) || (2 <= len___0
        && i___0 == 2)) || (1 <= len___0 && i___0 == 1)) || (0 == i___0 && i___0 ==
        0)) || (4 <= len___0 && 4 <= i___0)) || (3 <= len___0 && i___0 == 3)) || (2
        <= len___0 && i___0 == 2)) || (1 <= len___0 && i___0 == 1)) || (0 == i___0
        && i___0 == 0))) || ((-2147483647 <= top && 4 <= len___0) && 4 <= i___0))
        || ((-2147483647 <= top && 3 <= len___0) && i___0 == 3)) || ((-2147483647
        <= top && 2 <= len___0) && i___0 == 2)) || ((-2147483647 <= top && 1 <= len___0)
        && i___0 == 1)) || ((-2147483647 <= top && 0 == i___0) && i___0 == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: -128 <= d->rpl_optopt
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: 1 <= argc
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: d->rpl_optopt <= 127
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: 0 == long_only
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: 0 == posixly_correct
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: longind == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: longind == (int *)((void *)0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: long_only == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: long_only == posixly_correct
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: posixly_correct == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: d->__initialized == 0 || d->__initialized == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: d->__posixly_correct == 0 || d->__posixly_correct == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72726
        column: 9
        function: _getopt_internal_r
      value: ((unsigned int )d->__ordering == 0U || (unsigned int )d->__ordering ==
        1U) || (unsigned int )d->__ordering == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 86351
        column: 5
        function: main
      value: ((((-2147483644 <= argc && -2147483644 <= i) || (-2147483645 <= argc
        && -2147483645 <= i)) || (-2147483646 <= argc && -2147483646 <= i)) || (-2147483647
        <= argc && -2147483647 <= i)) || ((_Bool)1 == ok && ok == (_Bool)1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 20421
        column: 3
        function: last_component
      value: (_Bool)0 == saw_slash
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 20421
        column: 3
        function: last_component
      value: saw_slash == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 63330
        column: 3
        function: version_etc_va
      value: ((((4UL <= n_authors && n_authors <= 10UL) || n_authors == 3UL) || n_authors
        == 2UL) || n_authors == 1UL) || (0 == n_authors && n_authors == 0UL)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72115
        column: 7
        function: exchange
      value: -2147483647 <= middle
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72115
        column: 7
        function: exchange
      value: -128 <= d->rpl_optopt
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72115
        column: 7
        function: exchange
      value: bottom <= 2147483645
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72115
        column: 7
        function: exchange
      value: middle <= 2147483646
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72115
        column: 7
        function: exchange
      value: d->rpl_optopt <= 127
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72115
        column: 7
        function: exchange
      value: d->__initialized == 0 || d->__initialized == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72115
        column: 7
        function: exchange
      value: d->__posixly_correct == 0 || d->__posixly_correct == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72115
        column: 7
        function: exchange
      value: ((unsigned int )d->__ordering == 0U || (unsigned int )d->__ordering ==
        1U) || (unsigned int )d->__ordering == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72115
        column: 7
        function: exchange
      value: (((((-2147483646 <= top && ((((((((((((((((((((4 <= len && 4 <= i) ||
        (3 <= len && i == 3)) || (2 <= len && i == 2)) || (1 <= len && i == 1)) ||
        (0 == i && i == 0)) || (4 <= len && 4 <= i)) || (3 <= len && i == 3)) || (2
        <= len && i == 2)) || (1 <= len && i == 1)) || (0 == i && i == 0)) || (4 <=
        len && 4 <= i)) || (3 <= len && i == 3)) || (2 <= len && i == 2)) || (1 <=
        len && i == 1)) || (0 == i && i == 0)) || (4 <= len && 4 <= i)) || (3 <= len
        && i == 3)) || (2 <= len && i == 2)) || (1 <= len && i == 1)) || (0 == i &&
        i == 0))) || ((-2147483647 <= top && 4 <= len) && 4 <= i)) || ((-2147483647
        <= top && 3 <= len) && i == 3)) || ((-2147483647 <= top && 2 <= len) && i
        == 2)) || ((-2147483647 <= top && 1 <= len) && i == 1)) || ((-2147483647 <=
        top && 0 == i) && i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 35162
        column: 5
        function: umaxtostr
      value: (1UL <= i && (((i <= 1844674407370955UL || i <= 18446744073709551UL)
        || i <= 184467440737095516UL) || i <= 1844674407370955161UL)) || (char)0 ==
        *p
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: -128 <= d->rpl_optopt
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: d->rpl_optopt <= 127
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: -1 == indfound
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: 0 == long_only
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: 0 == posixly_correct
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: 0 == pfound
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: 0 == ambig_list
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: 0 == exact
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: argc == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: longind == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: longind == (int *)((void *)0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: long_only == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: long_only == posixly_correct
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: long_only == pfound
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: long_only == ambig_list
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: long_only == exact
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: posixly_correct == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: posixly_correct == pfound
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: posixly_correct == ambig_list
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: posixly_correct == exact
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: pfound == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: pfound == ambig_list
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: pfound == exact
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: ambig_list == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: ambig_list == exact
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: exact == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: indfound == -1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: d->__initialized == 0 || d->__initialized == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: d->__posixly_correct == 0 || d->__posixly_correct == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73239
        column: 13
        function: _getopt_internal_r
      value: ((unsigned int )d->__ordering == 0U || (unsigned int )d->__ordering ==
        1U) || (unsigned int )d->__ordering == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: -128 <= d->rpl_optopt
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: d->rpl_optopt <= 127
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: 0 == long_only
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: 0 == posixly_correct
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: 0 == pfound___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: 0 == exact___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: 0 == ambig
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: 0 == indfound___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: argc == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: longind == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: longind == (int *)((void *)0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: long_only == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: long_only == posixly_correct
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: long_only == pfound___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: long_only == exact___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: long_only == ambig
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: long_only == indfound___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: posixly_correct == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: posixly_correct == pfound___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: posixly_correct == exact___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: posixly_correct == ambig
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: posixly_correct == indfound___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: pfound___0 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: pfound___0 == exact___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: pfound___0 == ambig
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: pfound___0 == indfound___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: exact___0 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: exact___0 == ambig
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: exact___0 == indfound___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: ambig == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: ambig == indfound___0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: indfound___0 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: c != (char)58
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: c != (char)59
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: d->__initialized == 0 || d->__initialized == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: d->__posixly_correct == 0 || d->__posixly_correct == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74262
        column: 7
        function: _getopt_internal_r
      value: ((unsigned int )d->__ordering == 0U || (unsigned int )d->__ordering ==
        1U) || (unsigned int )d->__ordering == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: -128 <= d->rpl_optopt
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: -1 <= indfound
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: d->rpl_optopt <= 127
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: argc == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: longind == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: long_only == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: posixly_correct == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: exact == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: print_errors != 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: d->__initialized == 0 || d->__initialized == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: d->__posixly_correct == 0 || d->__posixly_correct == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: ((unsigned int )d->__ordering == 0U || (unsigned int )d->__ordering ==
        1U) || (unsigned int )d->__ordering == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73512
        column: 19
        function: _getopt_internal_r
      value: ((((((((((((((((((((((((((((((((((((((((((((((((5 <= option_index ||
        7 <= option_index) || 10 <= option_index) || 8 <= option_index) || 9 <= option_index)
        || 6 <= option_index) || 7 <= option_index) || 10 <= option_index) || 8 <=
        option_index) || 9 <= option_index) || 6 <= option_index) || 5 <= option_index)
        || 7 <= option_index) || 10 <= option_index) || 8 <= option_index) || 9 <=
        option_index) || 6 <= option_index) || 7 <= option_index) || 10 <= option_index)
        || 8 <= option_index) || 9 <= option_index) || 6 <= option_index) || 5 <=
        option_index) || 5 <= option_index) || 5 <= option_index) || 7 <= option_index)
        || 10 <= option_index) || 8 <= option_index) || 9 <= option_index) || 6 <=
        option_index) || 7 <= option_index) || 10 <= option_index) || 8 <= option_index)
        || 9 <= option_index) || 6 <= option_index) || 5 <= option_index) || 7 <=
        option_index) || 10 <= option_index) || 8 <= option_index) || 9 <= option_index)
        || 6 <= option_index) || 7 <= option_index) || 10 <= option_index) || 8 <=
        option_index) || 9 <= option_index) || 6 <= option_index) || (((((((((((((((((((((((((((((((((((((((((((((((((5
        <= option_index || 7 <= option_index) || 10 <= option_index) || 8 <= option_index)
        || 9 <= option_index) || 6 <= option_index) || 7 <= option_index) || 10 <=
        option_index) || 8 <= option_index) || 9 <= option_index) || 6 <= option_index)
        || 5 <= option_index) || 7 <= option_index) || 10 <= option_index) || 8 <=
        option_index) || 9 <= option_index) || 6 <= option_index) || 7 <= option_index)
        || 10 <= option_index) || 8 <= option_index) || 9 <= option_index) || 6 <=
        option_index) || 4 <= option_index) || 4 <= option_index) || 5 <= option_index)
        || 5 <= option_index) || 5 <= option_index) || 7 <= option_index) || 10 <=
        option_index) || 8 <= option_index) || 9 <= option_index) || 6 <= option_index)
        || 7 <= option_index) || 10 <= option_index) || 8 <= option_index) || 9 <=
        option_index) || 6 <= option_index) || 5 <= option_index) || 7 <= option_index)
        || 10 <= option_index) || 8 <= option_index) || 9 <= option_index) || 6 <=
        option_index) || 7 <= option_index) || 10 <= option_index) || 8 <= option_index)
        || 9 <= option_index) || 6 <= option_index) || 4 <= option_index) || 4 <=
        option_index)) || (((((((((((((((((((((((((((((((((((((((((((((((((((5 <=
        option_index || 7 <= option_index) || 10 <= option_index) || 8 <= option_index)
        || 9 <= option_index) || 6 <= option_index) || 7 <= option_index) || 10 <=
        option_index) || 8 <= option_index) || 9 <= option_index) || 6 <= option_index)
        || 5 <= option_index) || 7 <= option_index) || 10 <= option_index) || 8 <=
        option_index) || 9 <= option_index) || 6 <= option_index) || 7 <= option_index)
        || 10 <= option_index) || 8 <= option_index) || 9 <= option_index) || 6 <=
        option_index) || 4 <= option_index) || 4 <= option_index) || 3 <= option_index)
        || 5 <= option_index) || 5 <= option_index) || 5 <= option_index) || 7 <=
        option_index) || 10 <= option_index) || 8 <= option_index) || 9 <= option_index)
        || 6 <= option_index) || 7 <= option_index) || 10 <= option_index) || 8 <=
        option_index) || 9 <= option_index) || 6 <= option_index) || 5 <= option_index)
        || 7 <= option_index) || 10 <= option_index) || 8 <= option_index) || 9 <=
        option_index) || 6 <= option_index) || 7 <= option_index) || 10 <= option_index)
        || 8 <= option_index) || 9 <= option_index) || 6 <= option_index) || 4 <=
        option_index) || 4 <= option_index) || 3 <= option_index)) || (ambig_list
        == ambig_list->next && ((((((((((((((((((((((((((((((((((((((((((((((((((((((2
        <= option_index || 5 <= option_index) || 5 <= option_index) || 5 <= option_index)
        || 7 <= option_index) || 10 <= option_index) || 8 <= option_index) || 9 <=
        option_index) || 6 <= option_index) || 7 <= option_index) || 10 <= option_index)
        || 8 <= option_index) || 9 <= option_index) || 6 <= option_index) || 5 <=
        option_index) || 7 <= option_index) || 10 <= option_index) || 8 <= option_index)
        || 9 <= option_index) || 6 <= option_index) || 7 <= option_index) || 10 <=
        option_index) || 8 <= option_index) || 9 <= option_index) || 6 <= option_index)
        || 4 <= option_index) || 4 <= option_index) || 3 <= option_index) || 5 <=
        option_index) || 5 <= option_index) || 5 <= option_index) || 7 <= option_index)
        || 10 <= option_index) || 8 <= option_index) || 9 <= option_index) || 6 <=
        option_index) || 7 <= option_index) || 10 <= option_index) || 8 <= option_index)
        || 9 <= option_index) || 6 <= option_index) || 5 <= option_index) || 7 <=
        option_index) || 10 <= option_index) || 8 <= option_index) || 9 <= option_index)
        || 6 <= option_index) || 7 <= option_index) || 10 <= option_index) || 8 <=
        option_index) || 9 <= option_index) || 6 <= option_index) || 4 <= option_index)
        || 4 <= option_index) || 3 <= option_index))) || (ambig_list == & first &&
        ((((((((((((((((((((((((((((((((((((((((((((((((((((((2 <= option_index ||
        5 <= option_index) || 5 <= option_index) || 5 <= option_index) || 7 <= option_index)
        || 10 <= option_index) || 8 <= option_index) || 9 <= option_index) || 6 <=
        option_index) || 7 <= option_index) || 10 <= option_index) || 8 <= option_index)
        || 9 <= option_index) || 6 <= option_index) || 5 <= option_index) || 7 <=
        option_index) || 10 <= option_index) || 8 <= option_index) || 9 <= option_index)
        || 6 <= option_index) || 7 <= option_index) || 10 <= option_index) || 8 <=
        option_index) || 9 <= option_index) || 6 <= option_index) || 4 <= option_index)
        || 4 <= option_index) || 3 <= option_index) || 5 <= option_index) || 5 <=
        option_index) || 5 <= option_index) || 7 <= option_index) || 10 <= option_index)
        || 8 <= option_index) || 9 <= option_index) || 6 <= option_index) || 7 <=
        option_index) || 10 <= option_index) || 8 <= option_index) || 9 <= option_index)
        || 6 <= option_index) || 5 <= option_index) || 7 <= option_index) || 10 <=
        option_index) || 8 <= option_index) || 9 <= option_index) || 6 <= option_index)
        || 7 <= option_index) || 10 <= option_index) || 8 <= option_index) || 9 <=
        option_index) || 6 <= option_index) || 4 <= option_index) || 4 <= option_index)
        || 3 <= option_index))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: -128 <= d->rpl_optopt
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: d->rpl_optopt <= 127
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: argc == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: longind == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: longind == (int *)((void *)0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: long_only == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: posixly_correct == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: exact___0 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: c != (char)58
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: c != (char)59
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: d->__initialized == 0 || d->__initialized == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: d->__posixly_correct == 0 || d->__posixly_correct == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: ((unsigned int )d->__ordering == 0U || (unsigned int )d->__ordering ==
        1U) || (unsigned int )d->__ordering == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 74294
        column: 7
        function: _getopt_internal_r
      value: (((ambig == 0 || ambig == 1) && (((0 <= indfound___0 && 4 <= option_index___0)
        || (option_index___0 == 3 && ((indfound___0 == 0 || indfound___0 == 1) ||
        indfound___0 == 2))) || (option_index___0 == 2 && (indfound___0 == 0 || indfound___0
        == 1)))) || ((ambig == 0 && indfound___0 == 0) && option_index___0 == 1))
        || ((((((((((((((((((((((((((((((((0 == long_only && 0 == posixly_correct)
        && 0 == pfound___0) && 0 == exact___0) && 0 == ambig) && 0 == indfound___0)
        && 0 == option_index___0) && longopts == p___0) && long_only == posixly_correct)
        && long_only == pfound___0) && long_only == exact___0) && long_only == ambig)
        && long_only == indfound___0) && long_only == option_index___0) && posixly_correct
        == pfound___0) && posixly_correct == exact___0) && posixly_correct == ambig)
        && posixly_correct == indfound___0) && posixly_correct == option_index___0)
        && pfound___0 == 0) && pfound___0 == exact___0) && pfound___0 == ambig) &&
        pfound___0 == indfound___0) && pfound___0 == option_index___0) && exact___0
        == ambig) && exact___0 == indfound___0) && exact___0 == option_index___0)
        && ambig == 0) && ambig == indfound___0) && ambig == option_index___0) &&
        indfound___0 == 0) && indfound___0 == option_index___0) && option_index___0
        == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72079
        column: 3
        function: exchange
      value: -128 <= d->rpl_optopt
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72079
        column: 3
        function: exchange
      value: d->rpl_optopt <= 127
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72079
        column: 3
        function: exchange
      value: d->__initialized == 0 || d->__initialized == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72079
        column: 3
        function: exchange
      value: d->__posixly_correct == 0 || d->__posixly_correct == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 72079
        column: 3
        function: exchange
      value: ((unsigned int )d->__ordering == 0U || (unsigned int )d->__ordering ==
        1U) || (unsigned int )d->__ordering == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: -128 <= d->rpl_optopt
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: d->rpl_optopt <= 127
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: argc == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: longind == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: longind == (int *)((void *)0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: long_only == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: posixly_correct == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: exact == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: d->__initialized == 0 || d->__initialized == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: d->__posixly_correct == 0 || d->__posixly_correct == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: ((unsigned int )d->__ordering == 0U || (unsigned int )d->__ordering ==
        1U) || (unsigned int )d->__ordering == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-coreutils/instrumented_interval_cksum_comb.i
        line: 73272
        column: 13
        function: _getopt_internal_r
      value: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((4 <= option_index
        && ((-1 <= indfound && ambig_list == 0) || (ambig_list == newp && (indfound
        == -1 || indfound == 0)))) || ((5 <= option_index && ambig_list == newp) &&
        (indfound == -1 || indfound == 0))) || ((5 <= option_index && ambig_list ==
        newp) && (indfound == -1 || indfound == 0))) || ((5 <= option_index && ambig_list
        == newp) && (indfound == -1 || indfound == 0))) || ((7 <= option_index &&
        ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((10 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((8 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((9 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((6 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((7 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((10 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((8 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((9 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((6 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((5 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((7 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((10 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((8 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((9 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((6 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((7 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((10 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((8 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((9 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((6 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((4 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((4 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((4 <= option_index
        && ambig_list == newp) && (indfound == -1 || indfound == 0))) || ((-1 <= indfound
        && 5 <= option_index) && ambig_list == newp)) || ((5 <= option_index && ambig_list
        == newp) && (((indfound == -1 || indfound == 0) || indfound == 1) || indfound
        == 2))) || ((5 <= option_index && ambig_list == newp) && ((indfound == -1
        || indfound == 0) || indfound == 1))) || ((7 <= option_index && ambig_list
        == newp) && ((indfound == -1 || indfound == 0) || indfound == 1))) || ((10
        <= option_index && ambig_list == newp) && ((indfound == -1 || indfound ==
        0) || indfound == 1))) || ((8 <= option_index && ambig_list == newp) && ((indfound
        == -1 || indfound == 0) || indfound == 1))) || ((9 <= option_index && ambig_list
        == newp) && ((indfound == -1 || indfound == 0) || indfound == 1))) || ((6
        <= option_index && ambig_list == newp) && ((indfound == -1 || indfound ==
        0) || indfound == 1))) || ((7 <= option_index && ambig_list == newp) && (((indfound
        == -1 || indfound == 0) || indfound == 1) || indfound == 2))) || ((10 <= option_index
        && ambig_list == newp) && (((indfound == -1 || indfound == 0) || indfound
        == 1) || indfound == 2))) || ((8 <= option_index && ambig_list == newp) &&
        (((indfound == -1 || indfound == 0) || indfound == 1) || indfound == 2)))
        || ((9 <= option_index && ambig_list == newp) && (((indfound == -1 || indfound
        == 0) || indfound == 1) || indfound == 2))) || ((6 <= option_index && ambig_list
        == newp) && (((indfound == -1 || indfound == 0) || indfound == 1) || indfound
        == 2))) || ((5 <= option_index && ambig_list == newp) && ((indfound == -1
        || indfound == 0) || indfound == 1))) || ((7 <= option_index && ambig_list
        == newp) && ((indfound == -1 || indfound == 0) || indfound == 1))) || ((10
        <= option_index && ambig_list == newp) && ((indfound == -1 || indfound ==
        0) || indfound == 1))) || ((8 <= option_index && ambig_list == newp) && ((indfound
        == -1 || indfound == 0) || indfound == 1))) || ((9 <= option_index && ambig_list
        == newp) && ((indfound == -1 || indfound == 0) || indfound == 1))) || ((6
        <= option_index && ambig_list == newp) && ((indfound == -1 || indfound ==
        0) || indfound == 1))) || ((-1 <= indfound && 7 <= option_index) && ambig_list
        == newp)) || ((-1 <= indfound && 10 <= option_index) && ambig_list == newp))
        || ((-1 <= indfound && 8 <= option_index) && ambig_list == newp)) || ((-1
        <= indfound && 9 <= option_index) && ambig_list == newp)) || ((-1 <= indfound
        && 6 <= option_index) && ambig_list == newp)) || ((4 <= option_index && ambig_list
        == newp) && (((indfound == -1 || indfound == 0) || indfound == 1) || indfound
        == 2))) || ((4 <= option_index && ambig_list == newp) && ((indfound == -1
        || indfound == 0) || indfound == 1))) || ((4 <= option_index && ambig_list
        == newp) && ((indfound == -1 || indfound == 0) || indfound == 1))) || (option_index
        == 3 && ((((ambig_list == 0 && (((indfound == -1 || indfound == 0) || indfound
        == 1) || indfound == 2)) || (ambig_list == newp && (indfound == -1 || indfound
        == 0))) || (ambig_list == newp && (indfound == -1 || indfound == 0))) || (ambig_list
        == newp && ((indfound == -1 || indfound == 0) || indfound == 1))))) || (option_index
        == 2 && ((ambig_list == 0 && ((indfound == -1 || indfound == 0) || indfound
        == 1)) || (ambig_list == newp && (indfound == -1 || indfound == 0))))) ||
        ((ambig_list == 0 && option_index == 1) && (indfound == -1 || indfound ==
        0))) || ((((((((((((((((((((((((((-1 == indfound && 0 == long_only) && 0 ==
        posixly_correct) && 0 == pfound) && 0 == ambig_list) && 0 == exact) && 0 ==
        option_index) && longopts == p) && long_only == posixly_correct) && long_only
        == pfound) && long_only == ambig_list) && long_only == exact) && long_only
        == option_index) && posixly_correct == pfound) && posixly_correct == ambig_list)
        && posixly_correct == exact) && posixly_correct == option_index) && pfound
        == 0) && pfound == ambig_list) && pfound == exact) && pfound == option_index)
        && ambig_list == 0) && ambig_list == exact) && ambig_list == option_index)
        && exact == option_index) && indfound == -1) && option_index == 0)
      format: c_expression
