- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: c38a5818-12aa-4748-8576-e99956eb3007
    creation_time: 2025-03-22T08:48:35Z
    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'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i: ee90c95792b81649f087e170ece38fbab8d5281ca8435570782565b7b775a87f
      data_model: ILP32
      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/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5042
        function: main
      value: i <= 9999
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5042
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5042
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5042
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5042
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5042
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5042
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5042
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5042
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5042
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5042
        function: main
      value: ((((((((((((((((((((((((((((((((((((((((((_he_bkt_i <= 31U && ((((((((9
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (11 <= i && 12U <= bound))
        || ((6 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 512U)))
        || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U) && _he_bkt_i == 256U))
        || (((10 <= i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 256U))
        || ((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i <= 511U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 1023U) && _he_bkt_i == 32U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        <= 1023U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U) && _he_bkt_i
        == 128U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U) && _he_bkt_i
        == 64U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U) && _he_bkt_i
        == 512U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i
        == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i <= 511U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 128U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 64U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 512U)) || (((12 <=
        i && 13U <= bound) && _he_bkt_i <= 4294967294U) && _he_bkt_i == 256U)) ||
        (((9 <= i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 256U)) ||
        (((9 <= i && 10U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 256U)) ||
        (((9 <= i && 10U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 256U)) ||
        ((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i <= 255U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        <= 127U)) || ((11 <= i && 12U <= bound) && _he_bkt_i <= 63U)) || (((12 <=
        i && 13U <= bound) && _he_bkt_i <= 4294967294U) && _he_bkt_i == 32U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)) || (((12 <= i && 13U <=
        bound) && _he_bkt_i <= 4294967294U) && _he_bkt_i == 128U)) || (((12 <= i &&
        13U <= bound) && _he_bkt_i <= 4294967294U) && _he_bkt_i == 64U)) || (((12
        <= i && 13U <= bound) && _he_bkt_i <= 4294967294U) && _he_bkt_i == 512U))
        || (((9 <= i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 32U))
        || (((8 <= i && 9U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 32U)) ||
        (((7 <= i && 8U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 32U)) || ((9
        <= i && 10U <= bound) && _he_bkt_i <= 255U)) || ((8 <= i && 9U <= bound) &&
        _he_bkt_i <= 127U)) || ((7 <= i && 8U <= bound) && _he_bkt_i <= 63U)) || (((9
        <= i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 128U)) || (((8
        <= i && 9U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 128U)) || (((8
        <= i && 9U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 128U)) || (((9 <=
        i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 64U)) || (((8 <=
        i && 9U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 64U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 512U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 64U)) || (((10 <= i
        && 11U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 512U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4912
        function: main
      value: i <= 9999
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4912
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4912
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4912
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4912
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4912
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4912
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4912
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4912
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4912
        function: main
      value: (((((((((((((((((((((((((((((((((((((((((((((((((9 <= i && 10U <= bound)
        && _he_bkt_i <= 255U) || ((10 <= i && 11U <= bound) && _he_bkt_i <= 511U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)) || ((11 <= i &&
        12U <= bound) && _he_bkt_i <= 1023U)) || ((6 <= i && 7U <= bound) && _he_bkt_i
        <= 31U)) || ((7 <= i && 8U <= bound) && _he_bkt_i <= 63U)) || ((8 <= i &&
        9U <= bound) && _he_bkt_i <= 127U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 255U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 511U) && _he_bkt_i == 512U)) || (((12 <= i && 13U <= bound) && _he_bkt_i
        <= 4294967294U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 1023U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 31U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 63U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 127U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        <= 255U)) || ((12 <= i && 13U <= bound) && _he_bkt_i <= 511U)) || (((9 <=
        i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 128U)) || (((9 <=
        i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 32U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 256U)) || (((9 <=
        i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 64U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 128U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 32U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 256U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 64U)) || ((12 <=
        i && 13U <= bound) && _he_bkt_i <= 4294967294U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i <= 1023U)) || (((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)
        && _he_bkt_i == 128U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U)
        && _he_bkt_i == 128U)) || (((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)
        && _he_bkt_i == 32U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U)
        && _he_bkt_i == 32U)) || (((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)
        && _he_bkt_i == 256U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U)
        && _he_bkt_i == 256U)) || (((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)
        && _he_bkt_i == 64U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U)
        && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i <= 31U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i <= 63U)) || ((12 <= i && 13U <=
        bound) && _he_bkt_i <= 127U)) || (((9 <= i && 10U <= bound) && _he_bkt_i <=
        31U) && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i <= 31U)
        && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 31U)
        && _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i <= 31U) &&
        _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i
        == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i ==
        32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i ==
        256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 64U))
        || (((9 <= i && 10U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 128U))
        || (((8 <= i && 9U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 32U)) ||
        (((10 <= i && 11U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 256U)) ||
        (((8 <= i && 9U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 64U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: 0x9e3779b9u == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: _ha_hashv == 4276993779U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: _hj_j == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 1836
        function: main
      value: (users == altusers && ((((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((9
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (11 <= i && 12U <= bound))
        || ((6 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((11 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((7 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1))) || ((((((1U <= bound && 0 == i) &&
        0 == altusers) && i == 0) && i == altusers) && user == users) && altusers
        == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 39
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 39
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 39
        function: main
      value: (((((4UL == _hj_k && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _hj_k == 4U) && ((((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= i && 11U <= bound) && _he_bkt_i == 256U) || (12 <= i && 13U <= bound))
        || ((7 <= i && 8U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((8 <= i && 9U <= bound)
        && _he_bkt_i == 64U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 128U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i == 256U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i &&
        12U <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1))) || ((((((((1U <= bound && 0 == i)
        && 0 == users) && 0 == altusers) && i == 0) && i == users) && i == altusers)
        && users == 0) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3360
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3360
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3360
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3360
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3360
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3360
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3360
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3360
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3360
        function: main
      value: (((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= i && 11U <= bound) && _he_bkt_i == 256U) || (12 <= i && 13U <= bound))
        || ((7 <= i && 8U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((8 <= i && 9U <= bound)
        && _he_bkt_i == 64U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 128U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i == 256U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i &&
        12U <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3714
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3714
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3714
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3714
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3714
        function: main
      value: ((((4UL == _hj_k && users == altusers) && _hj_k == _hj_k) && _hj_k ==
        4U) && ((((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= i && 11U <= bound) && _he_bkt_i == 256U) || (12 <= i && 13U <= bound))
        || ((7 <= i && 8U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((8 <= i && 9U <= bound)
        && _he_bkt_i == 64U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 128U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i == 256U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i &&
        12U <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1))) || ((((((1U <= bound && 0 == i) &&
        0 == altusers) && i == 0) && i == altusers) && user == users) && altusers
        == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4976
        function: main
      value: i <= 9999
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4976
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4976
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4976
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4976
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4976
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4976
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4976
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4976
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4976
        function: main
      value: (((((((((((((((((((((((((((((((((((((((((((((((((9 <= i && 10U <= bound)
        && _he_bkt_i <= 255U) || ((10 <= i && 11U <= bound) && _he_bkt_i <= 511U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)) || ((11 <= i &&
        12U <= bound) && _he_bkt_i <= 1023U)) || ((6 <= i && 7U <= bound) && _he_bkt_i
        <= 31U)) || ((7 <= i && 8U <= bound) && _he_bkt_i <= 63U)) || ((8 <= i &&
        9U <= bound) && _he_bkt_i <= 127U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 255U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 511U) && _he_bkt_i == 512U)) || (((12 <= i && 13U <= bound) && _he_bkt_i
        <= 4294967294U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 1023U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 31U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 63U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 127U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        <= 255U)) || ((12 <= i && 13U <= bound) && _he_bkt_i <= 511U)) || (((9 <=
        i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 128U)) || (((9 <=
        i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 32U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 256U)) || (((9 <=
        i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 64U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 128U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 32U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 256U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 64U)) || ((12 <=
        i && 13U <= bound) && _he_bkt_i <= 4294967294U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i <= 1023U)) || (((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)
        && _he_bkt_i == 128U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U)
        && _he_bkt_i == 128U)) || (((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)
        && _he_bkt_i == 32U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U)
        && _he_bkt_i == 32U)) || (((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)
        && _he_bkt_i == 256U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U)
        && _he_bkt_i == 256U)) || (((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)
        && _he_bkt_i == 64U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U)
        && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i <= 31U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i <= 63U)) || ((12 <= i && 13U <=
        bound) && _he_bkt_i <= 127U)) || (((9 <= i && 10U <= bound) && _he_bkt_i <=
        31U) && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i <= 31U)
        && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 31U)
        && _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i <= 31U) &&
        _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i
        == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i ==
        32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i ==
        256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 64U))
        || (((9 <= i && 10U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 128U))
        || (((8 <= i && 9U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 32U)) ||
        (((10 <= i && 11U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 256U)) ||
        (((8 <= i && 9U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 64U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3578
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3578
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3578
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3578
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3578
        function: main
      value: ((((4UL == _hj_k && users == altusers) && _hj_k == _hj_k) && _hj_k ==
        4U) && ((((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= i && 11U <= bound) && _he_bkt_i == 256U) || (12 <= i && 13U <= bound))
        || ((7 <= i && 8U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((8 <= i && 9U <= bound)
        && _he_bkt_i == 64U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 128U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i == 256U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i &&
        12U <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1))) || ((((((1U <= bound && 0 == i) &&
        0 == altusers) && i == 0) && i == altusers) && user == users) && altusers
        == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: 0x9e3779b9u == _hj_i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: 0x9e3779b9u == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: 0xfeedbeefu == _ha_hashv
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: _ha_hashv == 4276993775U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: _hj_i == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: _hj_i == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: _hj_j == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 231
        function: main
      value: (users == altusers && ((((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((9
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (11 <= i && 12U <= bound))
        || ((6 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((11 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((7 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1))) || ((((((1U <= bound && 0 == i) &&
        0 == altusers) && i == 0) && i == altusers) && user == users) && altusers
        == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4768
        function: main
      value: i <= 9999
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4768
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4768
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4768
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4768
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4768
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4768
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4768
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4768
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4768
        function: main
      value: (((((((((((((((((((((((((((((((((((((((((((((((((9 <= i && 10U <= bound)
        && _he_bkt_i <= 256U) || ((10 <= i && 11U <= bound) && _he_bkt_i <= 512U))
        || (12 <= i && 13U <= bound)) || ((11 <= i && 12U <= bound) && _he_bkt_i <=
        1024U)) || ((6 <= i && 7U <= bound) && _he_bkt_i <= 32U)) || ((7 <= i && 8U
        <= bound) && _he_bkt_i <= 64U)) || ((8 <= i && 9U <= bound) && _he_bkt_i <=
        128U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 256U) && _he_bkt_i ==
        512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 512U) && _he_bkt_i ==
        512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 512U)) || (((11 <= i
        && 12U <= bound) && _he_bkt_i <= 1024U) && _he_bkt_i == 512U)) || (((11 <=
        i && 12U <= bound) && _he_bkt_i <= 32U) && _he_bkt_i == 512U)) || (((11 <=
        i && 12U <= bound) && _he_bkt_i <= 64U) && _he_bkt_i == 512U)) || (((11 <=
        i && 12U <= bound) && _he_bkt_i <= 128U) && _he_bkt_i == 512U)) || ((12 <=
        i && 13U <= bound) && _he_bkt_i <= 256U)) || ((12 <= i && 13U <= bound) &&
        _he_bkt_i <= 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i <= 256U) &&
        _he_bkt_i == 128U)) || (((9 <= i && 10U <= bound) && _he_bkt_i <= 256U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 256U) &&
        _he_bkt_i == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i <= 256U) &&
        _he_bkt_i == 64U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 512U) &&
        _he_bkt_i == 128U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 512U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 512U) &&
        _he_bkt_i == 256U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 512U) &&
        _he_bkt_i == 64U)) || (12 <= i && 13U <= bound)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i <= 1024U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1024U) && _he_bkt_i == 128U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i <= 1024U) && _he_bkt_i == 32U)) || ((12 <= i && 13U <=
        bound) && _he_bkt_i == 256U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 1024U) && _he_bkt_i == 256U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 64U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1024U) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i <= 32U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i <= 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        <= 128U)) || (((9 <= i && 10U <= bound) && _he_bkt_i <= 32U) && _he_bkt_i
        == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i <= 32U) && _he_bkt_i ==
        32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 32U) && _he_bkt_i ==
        256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i <= 32U) && _he_bkt_i == 64U))
        || (((9 <= i && 10U <= bound) && _he_bkt_i <= 64U) && _he_bkt_i == 128U))
        || (((7 <= i && 8U <= bound) && _he_bkt_i <= 64U) && _he_bkt_i == 32U)) ||
        (((10 <= i && 11U <= bound) && _he_bkt_i <= 64U) && _he_bkt_i == 256U)) ||
        (((8 <= i && 9U <= bound) && _he_bkt_i <= 64U) && _he_bkt_i == 64U)) || (((9
        <= i && 10U <= bound) && _he_bkt_i <= 128U) && _he_bkt_i == 128U)) || (((8
        <= i && 9U <= bound) && _he_bkt_i <= 128U) && _he_bkt_i == 32U)) || (((10
        <= i && 11U <= bound) && _he_bkt_i <= 128U) && _he_bkt_i == 256U)) || (((8
        <= i && 9U <= bound) && _he_bkt_i <= 128U) && _he_bkt_i == 64U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 749
        column: 5
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 749
        column: 5
        function: main
      value: (((((4UL == _hj_k && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _hj_k == 4U) && ((((((((i <= 10000 && bound <= 10000U) && ((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (12 <= i && 12U <= bound))
        || ((7 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (7 <= i && 7U <= bound))
        || ((9 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((8 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((11 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((12 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 11U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 11U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 256U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 12U <= bound)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((12 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        12U <= bound)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 12U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 12U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 9U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 128U)) || (((7 <= i && 7U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 32U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 256U)) || (((8 <= i && 8U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        64U)) || ((9 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 7U
        <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 10U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 8U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 9U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 8U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (i == 6 && bound ==
        6U)) || (i == 5 && bound == 5U)) || ((i == 4 && user == 0) && bound == 4U))
        || ((((((i <= 10000 && bound <= 10000U) && ((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (12 <= i && 12U <= bound))
        || ((7 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (7 <= i && 7U <= bound))
        || ((9 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((8 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((11 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((12 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 11U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 11U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 256U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 12U <= bound)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((12 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        12U <= bound)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 12U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 12U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 9U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 128U)) || (((7 <= i && 7U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 32U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 256U)) || (((8 <= i && 8U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        64U)) || ((9 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 7U
        <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 10U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 8U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 9U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 8U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (i == 6 && bound ==
        6U)) || (i == 5 && bound == 5U)) || (i == 4 && bound == 4U)) || ((i == 3 &&
        user == 0) && bound == 3U))) || (((((((i <= 10000 && bound <= 10000U) && ((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (12 <= i && 12U <= bound))
        || ((7 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (7 <= i && 7U <= bound))
        || ((9 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((8 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((11 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((12 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 11U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 11U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 256U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 12U <= bound)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((12 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        12U <= bound)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 12U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 12U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 9U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 128U)) || (((7 <= i && 7U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 32U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 256U)) || (((8 <= i && 8U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        64U)) || ((9 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 7U
        <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 10U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 8U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 9U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 8U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (i == 6 && bound ==
        6U)) || (i == 5 && bound == 5U)) || (i == 4 && bound == 4U)) || (i == 3 &&
        bound == 3U)) || ((i == 2 && user == 0) && bound == 2U))) || ((((((((i <=
        10000 && bound <= 10000U) && ((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (12 <= i && 12U <= bound))
        || ((7 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (7 <= i && 7U <= bound))
        || ((9 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((8 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((11 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((12 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 11U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 11U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 256U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 12U <= bound)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((12 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        12U <= bound)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 12U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 12U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 9U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 128U)) || (((7 <= i && 7U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 32U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 256U)) || (((8 <= i && 8U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        64U)) || ((9 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 7U
        <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 10U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 8U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 9U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 8U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (i == 6 && bound ==
        6U)) || (i == 5 && bound == 5U)) || (i == 4 && bound == 4U)) || (i == 3 &&
        bound == 3U)) || (i == 2 && bound == 2U)) || ((i == 1 && user == 0) && bound
        == 1U)))) || ((user == users && user == altusers) && ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        == i && 0 == user) && 0 == users) && 0 == altusers) && i == 0) && i == user)
        && i == users) && i == altusers) && user == 0) && users == 0) && altusers
        == 0) && bound == 0U) || (((((((((10 <= i && 10U <= bound) && i <= 10000)
        && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _he_bkt_i == 256U) && _hj_k == 4U)) || ((((((((12 <= i && 12U
        <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U)) || (((((((((7 <= i &&
        7U <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL ==
        _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 32U) && _hj_k ==
        4U)) || ((((((((7 <= i && 7U <= bound) && i <= 10000) && bound <= 10000U)
        && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k
        == 4U)) || (((((((((9 <= i && 9U <= bound) && i <= 10000) && bound <= 10000U)
        && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 128U) && _hj_k == 4U)) || (((((((((8 <= i && 8U <= bound) && i <= 10000)
        && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _he_bkt_i == 64U) && _hj_k == 4U)) || (((((((((11 <= i && 11U
        <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 512U) && _hj_k == 4U))
        || ((((((((((11 <= i && 11U <= bound) && i <= 10000) && bound <= 10000U) &&
        4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 256U) && _hj_k == 4U) && _he_bkt_i == 512U)) || (((((((((12 <= i && 12U
        <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _he_bkt_i == 512U))
        || ((((((((((11 <= i && 11U <= bound) && i <= 10000) && bound <= 10000U) &&
        4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 32U) && _hj_k == 4U) && _he_bkt_i == 512U)) || (((((((((11 <= i && 11U
        <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _he_bkt_i == 512U))
        || ((((((((((11 <= i && 11U <= bound) && i <= 10000) && bound <= 10000U) &&
        4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 128U) && _hj_k == 4U) && _he_bkt_i == 512U)) || ((((((((((11 <= i && 11U
        <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 64U) && _hj_k == 4U) &&
        _he_bkt_i == 512U)) || ((((((((((11 <= i && 11U <= bound) && i <= 10000) &&
        bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _he_bkt_i == 512U) && _hj_k == 4U) && _he_bkt_i == 512U)) ||
        (((((((((12 <= i && 12U <= bound) && i <= 10000) && bound <= 10000U) && 4UL
        == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 256U) && _hj_k == 4U)) || ((((((((((10 <= i && 10U <= bound) && i <= 10000)
        && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _he_bkt_i == 256U) && _hj_k == 4U) && _he_bkt_i == 128U)) ||
        ((((((((((10 <= i && 10U <= bound) && i <= 10000) && bound <= 10000U) && 4UL
        == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 256U) && _hj_k == 4U) && _he_bkt_i == 32U)) || ((((((((((10 <= i && 10U
        <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 256U) && _hj_k == 4U) &&
        _he_bkt_i == 256U)) || ((((((((((10 <= i && 10U <= bound) && i <= 10000) &&
        bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _he_bkt_i == 256U) && _hj_k == 4U) && _he_bkt_i == 64U)) || ((((((((12
        <= i && 12U <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k)
        && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U)) || (((((((((12
        <= i && 12U <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k)
        && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _he_bkt_i
        == 128U)) || (((((((((12 <= i && 12U <= bound) && i <= 10000) && bound <=
        10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _hj_k == 4U) && _he_bkt_i == 32U)) || (((((((((12 <= i && 12U <= bound)
        && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k
        == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _he_bkt_i == 256U)) || (((((((((12
        <= i && 12U <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k)
        && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _he_bkt_i
        == 64U)) || (((((((((12 <= i && 12U <= bound) && i <= 10000) && bound <= 10000U)
        && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 32U) && _hj_k == 4U)) || ((((((((12 <= i && 12U <= bound) && i <= 10000)
        && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _hj_k == 4U)) || (((((((((12 <= i && 12U <= bound) && i <= 10000)
        && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _he_bkt_i == 128U) && _hj_k == 4U)) || (((((((((12 <= i && 12U
        <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 64U) && _hj_k == 4U)) ||
        (((((((((12 <= i && 12U <= bound) && i <= 10000) && bound <= 10000U) && 4UL
        == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 512U) && _hj_k == 4U)) || ((((((((((9 <= i && 9U <= bound) && i <= 10000)
        && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _he_bkt_i == 32U) && _hj_k == 4U) && _he_bkt_i == 128U)) || ((((((((((7
        <= i && 7U <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) &&
        4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 32U) && _hj_k
        == 4U) && _he_bkt_i == 32U)) || ((((((((((10 <= i && 10U <= bound) && i <=
        10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U)
        && _hj_k == _hj_k) && _he_bkt_i == 32U) && _hj_k == 4U) && _he_bkt_i == 256U))
        || ((((((((((8 <= i && 8U <= bound) && i <= 10000) && bound <= 10000U) &&
        4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 32U) && _hj_k == 4U) && _he_bkt_i == 64U)) || (((((((((9 <= i && 9U <=
        bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _he_bkt_i == 128U))
        || (((((((((7 <= i && 7U <= bound) && i <= 10000) && bound <= 10000U) && 4UL
        == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k ==
        4U) && _he_bkt_i == 32U)) || (((((((((10 <= i && 10U <= bound) && i <= 10000)
        && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _hj_k == 4U) && _he_bkt_i == 256U)) || (((((((((8 <= i && 8U
        <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _he_bkt_i == 64U)) ||
        ((((((((((9 <= i && 9U <= bound) && i <= 10000) && bound <= 10000U) && 4UL
        == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 128U) && _hj_k == 4U) && _he_bkt_i == 128U)) || ((((((((((9 <= i && 9U
        <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 128U) && _hj_k == 4U) &&
        _he_bkt_i == 32U)) || ((((((((((10 <= i && 10U <= bound) && i <= 10000) &&
        bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _he_bkt_i == 128U) && _hj_k == 4U) && _he_bkt_i == 256U)) ||
        ((((((((((9 <= i && 9U <= bound) && i <= 10000) && bound <= 10000U) && 4UL
        == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 128U) && _hj_k == 4U) && _he_bkt_i == 64U)) || ((((((((((9 <= i && 9U <=
        bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 64U) && _hj_k == 4U) &&
        _he_bkt_i == 128U)) || ((((((((((11 <= i && 11U <= bound) && i <= 10000) &&
        bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _he_bkt_i == 512U) && _hj_k == 4U) && _he_bkt_i == 128U)) ||
        ((((((((((8 <= i && 8U <= bound) && i <= 10000) && bound <= 10000U) && 4UL
        == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 64U) && _hj_k == 4U) && _he_bkt_i == 32U)) || ((((((((((10 <= i && 10U
        <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 64U) && _hj_k == 4U) &&
        _he_bkt_i == 256U)) || ((((((((((8 <= i && 8U <= bound) && i <= 10000) &&
        bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _he_bkt_i == 64U) && _hj_k == 4U) && _he_bkt_i == 64U)) || ((((((((((11
        <= i && 11U <= bound) && i <= 10000) && bound <= 10000U) && 4UL == _hj_k)
        && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 512U)
        && _hj_k == 4U) && _he_bkt_i == 32U)) || ((((((((((11 <= i && 11U <= bound)
        && i <= 10000) && bound <= 10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k
        == 4U) && _hj_k == _hj_k) && _he_bkt_i == 512U) && _hj_k == 4U) && _he_bkt_i
        == 256U)) || ((((((((((11 <= i && 11U <= bound) && i <= 10000) && bound <=
        10000U) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _he_bkt_i == 512U) && _hj_k == 4U) && _he_bkt_i == 64U)) || ((((((4UL ==
        _hj_k && 4UL == _hj_k) && i == 6) && bound == 6U) && _hj_k == 4U) && _hj_k
        == _hj_k) && _hj_k == 4U)) || ((((((4UL == _hj_k && 4UL == _hj_k) && i ==
        5) && bound == 5U) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U)) ||
        ((((((4UL == _hj_k && 4UL == _hj_k) && i == 4) && bound == 4U) && _hj_k ==
        4U) && _hj_k == _hj_k) && _hj_k == 4U)) || ((((((4UL == _hj_k && 4UL == _hj_k)
        && i == 3) && bound == 3U) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k ==
        4U)) || ((((((4UL == _hj_k && 4UL == _hj_k) && i == 2) && bound == 2U) &&
        _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U)) || ((((((4UL == _hj_k &&
        4UL == _hj_k) && i == 1) && bound == 1U) && _hj_k == 4U) && _hj_k == _hj_k)
        && _hj_k == 4U)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 39
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 39
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 39
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 39
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 39
        function: main
      value: ((((4UL == _hj_k && users == altusers) && _hj_k == _hj_k) && _hj_k ==
        4U) && ((((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((9
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (11 <= i && 12U <= bound))
        || ((6 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((11 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((7 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1))) || ((((((1U <= bound && 0 == i) &&
        0 == altusers) && i == 0) && i == altusers) && user == users) && altusers
        == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: 1U <= bound
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: 0 == i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: 0 == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: i == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: i == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: user == users
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: altusers == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2691
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: 0x9e3779b9u == _hj_i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: 0x9e3779b9u == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: 0xfeedbeefu == _ha_hashv
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: _ha_hashv == 4276993775U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: _hj_i == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: _hj_i == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: _hj_j == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 227
        function: main
      value: (((4UL == _hj_k && _hj_k == _hj_k) && _hj_k == 4U) && ((((((i <= 9999
        && ((((((((((((((((((((((((((((((((((((((((((((((((((10 <= i && 11U <= bound)
        && _he_bkt_i == 256U) || (12 <= i && 13U <= bound)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound)) || ((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) ||
        ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <=
        bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 128U) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 64U) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 512U) && _he_bkt_i
        == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 256U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 128U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 256U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 64U)) || (12 <= i
        && 13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) ||
        ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 256U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 64U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i && 13U <=
        bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 64U))
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 256U))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i && 12U <= bound)
        && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i && 9U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) &&
        _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i == 5)) || (5U
        <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound && i == 2))
        || (2U <= bound && i == 1))) || ((((((((1U <= bound && 0 == i) && 0 == users)
        && 0 == altusers) && i == 0) && i == users) && i == altusers) && users ==
        0) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: 1U <= bound
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: 0 == i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: 0 == users
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: 0 == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: i == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: i == users
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: i == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: users == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: altusers == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2670
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4214
        function: main
      value: i <= 9999
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4214
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4214
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4214
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4214
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4214
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4214
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4214
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4214
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4214
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4214
        function: main
      value: (((((((((((((((((((((((((((((((((((((((((((((((((9 <= i && 10U <= bound)
        && _he_bkt_i == 256U) || (11 <= i && 12U <= bound)) || ((6 <= i && 7U <= bound)
        && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound)) || ((8 <= i && 9U <= bound)
        && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound) && _he_bkt_i == 64U)) ||
        ((10 <= i && 11U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U)) || ((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 128U) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 64U) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 512U) && _he_bkt_i
        == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 256U)) || (((9 <=
        i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 128U)) || (((9 <=
        i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 256U)) || (((9 <=
        i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 64U)) || (12 <= i
        && 13U <= bound)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 128U)) ||
        ((11 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((11 <= i && 12U <= bound)
        && _he_bkt_i == 256U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 64U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i && 13U <=
        bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 64U))
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 256U))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((8 <= i && 9U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((10 <= i && 11U <= bound)
        && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) &&
        _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((10 <= i && 11U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((10 <= i && 11U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 64U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4104
        function: main
      value: i <= 9999
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4104
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4104
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4104
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4104
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4104
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4104
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4104
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4104
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 4104
        function: main
      value: (((((((((((((((((((((((((((((((((((((((((((((((((10 <= i && 11U <= bound)
        && _he_bkt_i == 256U) || (12 <= i && 13U <= bound)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound)) || ((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) ||
        ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <=
        bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 128U) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 64U) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 512U) && _he_bkt_i
        == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 256U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 128U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 256U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 64U)) || (12 <= i
        && 13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) ||
        ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 256U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 64U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i && 13U <=
        bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 64U))
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 256U))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i && 12U <= bound)
        && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i && 9U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) &&
        _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 64U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 1832
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 1832
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 1832
        function: main
      value: 0x9e3779b9u == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 1832
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 1832
        function: main
      value: _ha_hashv == 4276993779U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 1832
        function: main
      value: _hj_j == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 1832
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 1832
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 1832
        function: main
      value: (((4UL == _hj_k && _hj_k == _hj_k) && _hj_k == 4U) && ((((((i <= 9999
        && ((((((((((((((((((((((((((((((((((((((((((((((((((10 <= i && 11U <= bound)
        && _he_bkt_i == 256U) || (12 <= i && 13U <= bound)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound)) || ((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) ||
        ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <=
        bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 128U) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 64U) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 512U) && _he_bkt_i
        == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 256U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 128U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 256U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 64U)) || (12 <= i
        && 13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) ||
        ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 256U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 64U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i && 13U <=
        bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 64U))
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 256U))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i && 12U <= bound)
        && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i && 9U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) &&
        _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i == 5)) || (5U
        <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound && i == 2))
        || (2U <= bound && i == 1))) || ((((((((1U <= bound && 0 == i) && 0 == users)
        && 0 == altusers) && i == 0) && i == users) && i == altusers) && users ==
        0) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4894
        function: main
      value: i <= 9999
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4894
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4894
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4894
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4894
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4894
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4894
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4894
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4894
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4894
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 4894
        function: main
      value: ((((((((((((((((((((((((((((((((((((((((((_he_bkt_i <= 32U && ((((((((9
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (11 <= i && 12U <= bound))
        || ((6 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 512U)))
        || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1024U) && _he_bkt_i == 256U))
        || (((10 <= i && 11U <= bound) && _he_bkt_i <= 512U) && _he_bkt_i == 256U))
        || ((11 <= i && 12U <= bound) && _he_bkt_i <= 1024U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i <= 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 1024U) && _he_bkt_i == 32U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        <= 1024U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1024U) && _he_bkt_i
        == 128U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1024U) && _he_bkt_i
        == 64U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1024U) && _he_bkt_i
        == 512U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 512U) && _he_bkt_i
        == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i <= 512U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 512U) && _he_bkt_i == 128U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 512U) && _he_bkt_i == 64U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 512U) && _he_bkt_i == 512U)) || ((12 <=
        i && 13U <= bound) && _he_bkt_i == 256U)) || (((9 <= i && 10U <= bound) &&
        _he_bkt_i <= 256U) && _he_bkt_i == 256U)) || (((9 <= i && 10U <= bound) &&
        _he_bkt_i <= 128U) && _he_bkt_i == 256U)) || (((9 <= i && 10U <= bound) &&
        _he_bkt_i <= 64U) && _he_bkt_i == 256U)) || (12 <= i && 13U <= bound)) ||
        ((11 <= i && 12U <= bound) && _he_bkt_i <= 256U)) || ((11 <= i && 12U <= bound)
        && _he_bkt_i <= 128U)) || ((11 <= i && 12U <= bound) && _he_bkt_i <= 64U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i && 13U <=
        bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i <= 256U) && _he_bkt_i
        == 32U)) || (((8 <= i && 9U <= bound) && _he_bkt_i <= 128U) && _he_bkt_i ==
        32U)) || (((7 <= i && 8U <= bound) && _he_bkt_i <= 64U) && _he_bkt_i == 32U))
        || ((9 <= i && 10U <= bound) && _he_bkt_i <= 256U)) || ((8 <= i && 9U <= bound)
        && _he_bkt_i <= 128U)) || ((7 <= i && 8U <= bound) && _he_bkt_i <= 64U)) ||
        (((9 <= i && 10U <= bound) && _he_bkt_i <= 256U) && _he_bkt_i == 128U)) ||
        (((8 <= i && 9U <= bound) && _he_bkt_i <= 128U) && _he_bkt_i == 128U)) ||
        (((8 <= i && 9U <= bound) && _he_bkt_i <= 64U) && _he_bkt_i == 128U)) || (((9
        <= i && 10U <= bound) && _he_bkt_i <= 256U) && _he_bkt_i == 64U)) || (((8
        <= i && 9U <= bound) && _he_bkt_i <= 128U) && _he_bkt_i == 64U)) || (((10
        <= i && 11U <= bound) && _he_bkt_i <= 256U) && _he_bkt_i == 512U)) || (((10
        <= i && 11U <= bound) && _he_bkt_i <= 128U) && _he_bkt_i == 512U)) || (((7
        <= i && 8U <= bound) && _he_bkt_i <= 64U) && _he_bkt_i == 64U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 64U) && _he_bkt_i == 512U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2467
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2467
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2467
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2467
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2467
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 2467
        function: main
      value: (((4UL == _hj_k && _hj_k == _hj_k) && _hj_k == 4U) && ((((((i <= 9999
        && ((((((((((((((((((((((((((((((((((((((((((((((((((10 <= i && 11U <= bound)
        && _he_bkt_i == 256U) || (12 <= i && 13U <= bound)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound)) || ((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) ||
        ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <=
        bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 128U) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 64U) && _he_bkt_i
        == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i == 512U) && _he_bkt_i
        == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 256U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 128U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 256U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 64U)) || (12 <= i
        && 13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) ||
        ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 256U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 64U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i && 13U <=
        bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 64U))
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 256U))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i && 12U <= bound)
        && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i && 9U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound)
        && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) &&
        _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 12U <= bound) &&
        _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i == 5)) || (5U
        <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound && i == 2))
        || (2U <= bound && i == 1))) || ((((((((1U <= bound && 0 == i) && 0 == users)
        && 0 == altusers) && i == 0) && i == users) && i == altusers) && users ==
        0) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3809
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3809
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3809
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3809
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3809
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3809
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3809
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3809
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3809
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3809
        function: main
      value: ((((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((9
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (11 <= i && 12U <= bound))
        || ((6 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((11 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((7 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1)) || ((((1U <= bound && 0 == i) && i
        == 0) && user == users) && user == altusers)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3631
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3631
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3631
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3631
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 746
        column: 3631
        function: main
      value: ((((4UL == _hj_k && users == altusers) && _hj_k == _hj_k) && _hj_k ==
        4U) && ((((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= i && 11U <= bound) && _he_bkt_i == 256U) || (12 <= i && 13U <= bound))
        || ((7 <= i && 8U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((8 <= i && 9U <= bound)
        && _he_bkt_i == 64U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((12 <= i && 13U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 128U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || ((12 <= i
        && 13U <= bound) && _he_bkt_i == 256U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i &&
        12U <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 12U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1))) || ((((((1U <= bound && 0 == i) &&
        0 == altusers) && i == 0) && i == altusers) && user == users) && altusers
        == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2471
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2471
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2471
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2471
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2471
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2471
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2471
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2471
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 2471
        function: main
      value: (users == altusers && ((((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((9
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (11 <= i && 12U <= bound))
        || ((6 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((11 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((7 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1))) || ((((((1U <= bound && 0 == i) &&
        0 == altusers) && i == 0) && i == altusers) && user == users) && altusers
        == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 739
        column: 5
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 739
        column: 5
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 739
        column: 5
        function: main
      value: (((((((4UL == _hj_k && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _hj_key == & user->id) && _hj_k == 4U) && _hj_key == & user->cookie) &&
        (((((((i <= 10000 && ((((((((((((((((((((((((((((((((((((((((((((((((((10
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (12 <= i && 12U <= bound))
        || ((7 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (7 <= i && 7U <= bound))
        || ((9 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((8 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((11 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((12 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 11U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 11U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 11U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 256U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 12U <= bound)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((12 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((12 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        12U <= bound)) || ((12 <= i && 12U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 12U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 12U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 9U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 128U)) || (((7 <= i && 7U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 32U)) || (((10 <= i && 10U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 256U)) || (((8 <= i && 8U <= bound) && _he_bkt_i == 32U) && _he_bkt_i ==
        64U)) || ((9 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 7U
        <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 10U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 8U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 9U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((11 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((8 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 8U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((11 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        6)) || (5U <= bound && i == 5)) || (4U <= bound && i == 4)) || (3U <= bound
        && i == 3)) || (2U <= bound && i == 2)) || (((1U <= bound && i == 1) && user
        == users) && user == altusers))) || (((((((0 == i && 0 == users) && 0 == altusers)
        && i == 0) && i == users) && i == altusers) && users == 0) && altusers ==
        0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3663
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3663
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3663
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3663
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3663
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3663
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3663
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3663
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3663
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3663
        function: main
      value: ((((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((9
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (11 <= i && 12U <= bound))
        || ((6 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((11 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((7 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1)) || ((((1U <= bound && 0 == i) && i
        == 0) && user == users) && user == altusers)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5106
        function: main
      value: i <= 9999
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5106
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5106
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5106
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5106
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5106
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5106
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5106
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5106
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5106
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 5106
        function: main
      value: ((((((((((((((((((((((((((((((((((((((((((_he_bkt_i <= 31U && ((((((((9
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (11 <= i && 12U <= bound))
        || ((6 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 512U)))
        || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U) && _he_bkt_i == 256U))
        || (((10 <= i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 256U))
        || ((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i <= 511U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        <= 1023U) && _he_bkt_i == 32U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        <= 1023U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U) && _he_bkt_i
        == 128U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U) && _he_bkt_i
        == 64U)) || (((11 <= i && 12U <= bound) && _he_bkt_i <= 1023U) && _he_bkt_i
        == 512U)) || (((10 <= i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i
        == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i <= 511U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 128U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 64U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 511U) && _he_bkt_i == 512U)) || (((12 <=
        i && 13U <= bound) && _he_bkt_i <= 4294967294U) && _he_bkt_i == 256U)) ||
        (((9 <= i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 256U)) ||
        (((9 <= i && 10U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 256U)) ||
        (((9 <= i && 10U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 256U)) ||
        ((12 <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i <= 255U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        <= 127U)) || ((11 <= i && 12U <= bound) && _he_bkt_i <= 63U)) || (((12 <=
        i && 13U <= bound) && _he_bkt_i <= 4294967294U) && _he_bkt_i == 32U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i <= 4294967294U)) || (((12 <= i && 13U <=
        bound) && _he_bkt_i <= 4294967294U) && _he_bkt_i == 128U)) || (((12 <= i &&
        13U <= bound) && _he_bkt_i <= 4294967294U) && _he_bkt_i == 64U)) || (((12
        <= i && 13U <= bound) && _he_bkt_i <= 4294967294U) && _he_bkt_i == 512U))
        || (((9 <= i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 32U))
        || (((8 <= i && 9U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 32U)) ||
        (((7 <= i && 8U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 32U)) || ((9
        <= i && 10U <= bound) && _he_bkt_i <= 255U)) || ((8 <= i && 9U <= bound) &&
        _he_bkt_i <= 127U)) || ((7 <= i && 8U <= bound) && _he_bkt_i <= 63U)) || (((9
        <= i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 128U)) || (((8
        <= i && 9U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 128U)) || (((8
        <= i && 9U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 128U)) || (((9 <=
        i && 10U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 64U)) || (((8 <=
        i && 9U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 64U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 255U) && _he_bkt_i == 512U)) || (((10 <=
        i && 11U <= bound) && _he_bkt_i <= 127U) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 64U)) || (((10 <= i
        && 11U <= bound) && _he_bkt_i <= 63U) && _he_bkt_i == 512U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3721
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3721
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3721
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3721
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3721
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3721
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3721
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3721
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3721
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3721
        function: main
      value: ((((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((9
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (11 <= i && 12U <= bound))
        || ((6 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((11 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((7 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1)) || ((((1U <= bound && 0 == i) && i
        == 0) && user == users) && user == altusers)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3419
        function: main
      value: bound <= 10000U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3419
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3419
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3419
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3419
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3419
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3419
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3419
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3419
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test4-1.i
        line: 747
        column: 3419
        function: main
      value: (((((i <= 9999 && ((((((((((((((((((((((((((((((((((((((((((((((((((9
        <= i && 10U <= bound) && _he_bkt_i == 256U) || (11 <= i && 12U <= bound))
        || ((6 <= i && 7U <= bound) && _he_bkt_i == 32U)) || (6 <= i && 7U <= bound))
        || ((8 <= i && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 8U <= bound)
        && _he_bkt_i == 64U)) || ((10 <= i && 11U <= bound) && _he_bkt_i == 512U))
        || (((11 <= i && 12U <= bound) && _he_bkt_i == 256U) && _he_bkt_i == 512U))
        || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U
        <= bound) && _he_bkt_i == 32U) && _he_bkt_i == 512U)) || ((11 <= i && 12U
        <= bound) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U) && _he_bkt_i == 512U)) || (((11 <= i && 12U <= bound) && _he_bkt_i
        == 512U) && _he_bkt_i == 512U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 256U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 256U) && _he_bkt_i
        == 64U)) || (12 <= i && 13U <= bound)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 128U)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 32U)) || ((11 <= i
        && 12U <= bound) && _he_bkt_i == 256U)) || ((11 <= i && 12U <= bound) && _he_bkt_i
        == 64U)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 32U)) || (12 <= i &&
        13U <= bound)) || ((12 <= i && 13U <= bound) && _he_bkt_i == 128U)) || ((12
        <= i && 13U <= bound) && _he_bkt_i == 64U)) || ((12 <= i && 13U <= bound)
        && _he_bkt_i == 512U)) || (((9 <= i && 10U <= bound) && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || (((7 <= i && 8U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && _he_bkt_i == 32U) &&
        _he_bkt_i == 256U)) || (((8 <= i && 9U <= bound) && _he_bkt_i == 32U) && _he_bkt_i
        == 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) && _he_bkt_i
        == 256U)) || ((8 <= i && 9U <= bound) && _he_bkt_i == 64U)) || (((9 <= i &&
        10U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || (((10 <= i &&
        11U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 256U)) || (((8 <= i &&
        9U <= bound) && _he_bkt_i == 128U) && _he_bkt_i == 64U)) || (((9 <= i && 10U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 512U) && _he_bkt_i == 128U)) || (((7 <= i && 8U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((8 <= i && 9U <=
        bound) && _he_bkt_i == 64U) && _he_bkt_i == 64U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 32U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 256U)) || (((10 <= i && 11U <=
        bound) && _he_bkt_i == 512U) && _he_bkt_i == 64U))) || (6U <= bound && i ==
        5)) || (5U <= bound && i == 4)) || (4U <= bound && i == 3)) || (3U <= bound
        && i == 2)) || (2U <= bound && i == 1)
      format: c_expression
