- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: b6eaa88c-86aa-42c7-9509-47b0927b104d
    creation_time: 2025-03-22T08:44:17Z
    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_test2-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i: 0fdcb64865aeb8184805095bc8dbe7392078d445cf902388dac9d1ca4533bb8c
      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_test2-2.i
        line: 826
        column: 3062
        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_test2-2.i
        line: 826
        column: 3062
        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_test2-2.i
        line: 826
        column: 3062
        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_test2-2.i
        line: 826
        column: 3062
        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_test2-2.i
        line: 826
        column: 3062
        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_test2-2.i
        line: 826
        column: 3062
        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_test2-2.i
        line: 826
        column: 3062
        function: main
      value: _hj_key == & 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_test2-2.i
        line: 826
        column: 3062
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 826
        column: 3062
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9999 && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && (((8U <= bound && _he_bkt_i ==
        64U) || (9U <= bound && _he_bkt_i == 128U)) || 7U <= bound)) || ((i <= 5 &&
        *((int *)_hj_key) <= 5) && bound == 6U)) || (((12U <= bound && i <= 9999)
        && bound <= 10000U) && *((int *)_hj_key) <= 9999)) || ((((11U <= bound &&
        i <= 9999) && bound <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i
        == 512U)) || ((((7U <= bound && i <= 9999) && bound <= 10000U) && *((int *)_hj_key)
        <= 9999) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9999) && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i == 256U))) || (((0 ==
        i && i == 0) && bound == 2U) && *((int *)_hj_key) == 0)) || ((((0 <= i &&
        0 <= *((int *)_hj_key)) && i <= 2) && *((int *)_hj_key) <= 2) && bound ==
        3U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key)
        <= 4) && bound == 5U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 3)
        && *((int *)_hj_key) <= 3) && bound == 4U)) || ((((0 == i && i == 0) && user
        == users) && bound == 1U) && *((int *)_hj_key) == 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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 4104
        function: main
      value: (((((((8 <= i && 9U <= bound) && _he_bkt_i == 64U) || ((9 <= i && 10U
        <= bound) && _he_bkt_i == 128U)) || (6 <= i && 7U <= bound)) || (12 <= i &&
        13U <= bound)) || ((11 <= i && 12U <= bound) && _he_bkt_i == 512U)) || ((7
        <= i && 8U <= bound) && _he_bkt_i == 32U)) || ((10 <= i && 11U <= bound) &&
        _he_bkt_i == 256U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 227
        function: main
      value: ((((((((((i <= 9999 && ((((8 <= i && 9U <= bound) && _he_bkt_i == 64U)
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || (6 <= i && 7U <= bound)))
        || (6U <= bound && i == 5)) || ((12 <= i && 13U <= bound) && i <= 9999)) ||
        (((11 <= i && 12U <= bound) && i <= 9999) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9999) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9999) && _he_bkt_i == 256U)) || (2U <= bound && i == 1))
        || (3U <= bound && i == 2)) || (5U <= bound && i == 4)) || (4U <= bound &&
        i == 3)) || (((((1U <= bound && 0 == i) && 0 == users) && i == 0) && i ==
        users) && 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_test2-2.i
        line: 831
        column: 757
        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_test2-2.i
        line: 831
        column: 757
        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_test2-2.i
        line: 831
        column: 757
        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_test2-2.i
        line: 831
        column: 757
        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_test2-2.i
        line: 831
        column: 757
        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_test2-2.i
        line: 831
        column: 757
        function: main
      value: _hd_hh_del == & user->hh
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i
        line: 831
        column: 757
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 831
        column: 757
        function: main
      value: ((((_hj_key == & i && ((((((((((((i <= 10001 && bound <= 10000U) && *((int
        *)_hj_key) <= 10001) && (((((8 <= i && 8 <= *((int *)_hj_key)) && 8U <= bound)
        && _he_bkt_i == 64U) || (((9 <= i && 9 <= *((int *)_hj_key)) && 9U <= bound)
        && _he_bkt_i == 128U)) || ((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound)))
        || ((((6 <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int *)_hj_key) <=
        7) && bound == 6U)) || (((((12 <= i && 12 <= *((int *)_hj_key)) && 12U <=
        bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001))
        || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 512U))
        || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 32U)) ||
        ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 256U))
        || ((i == 2 && bound == 2U) && *((int *)_hj_key) == 2)) || ((((3 <= i && 3
        <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key) <= 4) && bound == 3U))
        || ((((5 <= i && 5 <= *((int *)_hj_key)) && i <= 6) && *((int *)_hj_key) <=
        6) && bound == 5U)) || ((((4 <= i && 4 <= *((int *)_hj_key)) && i <= 5) &&
        *((int *)_hj_key) <= 5) && bound == 4U))) || (((((((((((((((((((((((i <= 10001
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && (((((8 <= i && 8 <=
        *((int *)_hj_key)) && 8U <= bound) && _he_bkt_i == 64U) || (((9 <= i && 9
        <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U)) || (((9 <= i
        && 9 <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U))) || (((((6
        <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int *)_hj_key) <= 7) && bound
        == 6U) && temp == 0)) || (((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound)
        && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || (((((7
        <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001) && bound <=
        10000U) && *((int *)_hj_key) <= 10001)) || ((((6 <= i && 6 <= *((int *)_hj_key))
        && i <= 7) && *((int *)_hj_key) <= 7) && bound == 6U)) || (((((12 <= i &&
        12 <= *((int *)_hj_key)) && 12U <= bound) && i <= 10001) && bound <= 10000U)
        && *((int *)_hj_key) <= 10001)) || (((((12 <= i && 12 <= *((int *)_hj_key))
        && 12U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001)) || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 512U)) || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 32U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i ==
        32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i ==
        256U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 256U)) || ((((((8 <= i && 8 <= *((int *)_hj_key)) && 8U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 64U)) || ((((((9 <= i && 9 <= *((int *)_hj_key)) && 9U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i ==
        128U)) || (((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || (((((5 <= i && 5 <=
        *((int *)_hj_key)) && i <= 6) && *((int *)_hj_key) <= 6) && bound == 5U) &&
        temp == 0)) || (((((12 <= i && 12 <= *((int *)_hj_key)) && 12U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || ((((((11
        <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i <= 10001) && bound
        <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 512U)) || ((((((7
        <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001) && bound <=
        10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 32U)) || ((((((10 <=
        i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <= 10001) && bound <=
        10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 256U))) || ((((((((((i
        <= 10001 && bound <= 10000U) && *((int *)_hj_key) <= 10001) && (((((8 <= i
        && 8 <= *((int *)_hj_key)) && 8U <= bound) && _he_bkt_i == 64U) || (((9 <=
        i && 9 <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U)) || ((7
        <= i && 7 <= *((int *)_hj_key)) && 7U <= bound))) || ((((6 <= i && 6 <= *((int
        *)_hj_key)) && i <= 7) && *((int *)_hj_key) <= 7) && bound == 6U)) || (((((12
        <= i && 12 <= *((int *)_hj_key)) && 12U <= bound) && i <= 10001) && bound
        <= 10000U) && *((int *)_hj_key) <= 10001)) || ((((((11 <= i && 11 <= *((int
        *)_hj_key)) && 11U <= bound) && i <= 10001) && bound <= 10000U) && *((int
        *)_hj_key) <= 10001) && _he_bkt_i == 512U)) || ((((((7 <= i && 7 <= *((int
        *)_hj_key)) && 7U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key)
        <= 10001) && _he_bkt_i == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key))
        && 10U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001) && _he_bkt_i == 256U)) || ((((5 <= i && 5 <= *((int *)_hj_key)) &&
        i <= 6) && *((int *)_hj_key) <= 6) && bound == 5U)) || (((((4 <= i && 4 <=
        *((int *)_hj_key)) && i <= 5) && *((int *)_hj_key) <= 5) && bound == 4U) &&
        temp == 0))) || (_hj_key == & i && (((((((((((i <= 10001 && bound <= 10000U)
        && *((int *)_hj_key) <= 10001) && (((((8 <= i && 8 <= *((int *)_hj_key)) &&
        8U <= bound) && _he_bkt_i == 64U) || (((9 <= i && 9 <= *((int *)_hj_key))
        && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 7 <= *((int *)_hj_key))
        && 7U <= bound))) || ((((6 <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int
        *)_hj_key) <= 7) && bound == 6U)) || (((((12 <= i && 12 <= *((int *)_hj_key))
        && 12U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001)) || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 256U)) || (((((3 <= i && 3 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key)
        <= 4) && bound == 3U) && temp == 0)) || ((((5 <= i && 5 <= *((int *)_hj_key))
        && i <= 6) && *((int *)_hj_key) <= 6) && bound == 5U)) || ((((4 <= i && 4
        <= *((int *)_hj_key)) && i <= 5) && *((int *)_hj_key) <= 5) && bound == 4U))))
        || (_hj_key == & i && ((((((((((((i <= 10001 && bound <= 10000U) && *((int
        *)_hj_key) <= 10001) && (((((8 <= i && 8 <= *((int *)_hj_key)) && 8U <= bound)
        && _he_bkt_i == 64U) || (((9 <= i && 9 <= *((int *)_hj_key)) && 9U <= bound)
        && _he_bkt_i == 128U)) || ((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound)))
        || ((((6 <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int *)_hj_key) <=
        7) && bound == 6U)) || (((((12 <= i && 12 <= *((int *)_hj_key)) && 12U <=
        bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001))
        || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 512U))
        || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 32U)) ||
        ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 256U))
        || (((i == 2 && bound == 2U) && temp == 0) && *((int *)_hj_key) == 2)) ||
        ((((3 <= i && 3 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key) <= 4)
        && bound == 3U)) || ((((5 <= i && 5 <= *((int *)_hj_key)) && i <= 6) && *((int
        *)_hj_key) <= 6) && bound == 5U)) || ((((4 <= i && 4 <= *((int *)_hj_key))
        && i <= 5) && *((int *)_hj_key) <= 5) && bound == 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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 4768
        function: main
      value: (((((((8 <= i && 9U <= bound) && _he_bkt_i <= 128U) || ((7 <= i && 8U
        <= bound) && _he_bkt_i <= 64U)) || ((9 <= i && 10U <= bound) && _he_bkt_i
        <= 256U)) || ((6 <= i && 7U <= bound) && _he_bkt_i <= 32U)) || ((11 <= i &&
        12U <= bound) && _he_bkt_i <= 1024U)) || (12 <= i && 13U <= bound)) || ((10
        <= i && 11U <= bound) && _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_test2-2.i
        line: 826
        column: 2612
        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_test2-2.i
        line: 826
        column: 2612
        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_test2-2.i
        line: 826
        column: 2612
        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_test2-2.i
        line: 826
        column: 2612
        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_test2-2.i
        line: 826
        column: 2612
        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_test2-2.i
        line: 826
        column: 2612
        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_test2-2.i
        line: 826
        column: 2612
        function: main
      value: _hj_key == & 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_test2-2.i
        line: 826
        column: 2612
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 826
        column: 2612
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9999 && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && (((8U <= bound && _he_bkt_i ==
        64U) || (9U <= bound && _he_bkt_i == 128U)) || 7U <= bound)) || ((i <= 5 &&
        *((int *)_hj_key) <= 5) && bound == 6U)) || (((12U <= bound && i <= 9999)
        && bound <= 10000U) && *((int *)_hj_key) <= 9999)) || ((((11U <= bound &&
        i <= 9999) && bound <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i
        == 512U)) || ((((7U <= bound && i <= 9999) && bound <= 10000U) && *((int *)_hj_key)
        <= 9999) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9999) && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i == 256U))) || (((0 ==
        i && i == 0) && bound == 2U) && *((int *)_hj_key) == 0)) || ((((0 <= i &&
        0 <= *((int *)_hj_key)) && i <= 2) && *((int *)_hj_key) <= 2) && bound ==
        3U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key)
        <= 4) && bound == 5U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 3)
        && *((int *)_hj_key) <= 3) && bound == 4U)) || ((((0 == i && i == 0) && user
        == users) && bound == 1U) && *((int *)_hj_key) == 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_test2-2.i
        line: 816
        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_test2-2.i
        line: 816
        column: 5
        function: main
      value: (((4UL == _hj_k && _hj_k == 4U) && _hj_key == & user->id) && (((((((((((i
        <= 10000 && ((((8 <= i && 8U <= bound) && _he_bkt_i == 64U) || ((9 <= i &&
        9U <= bound) && _he_bkt_i == 128U)) || (7 <= i && 7U <= bound))) || (6U <=
        bound && i == 6)) || ((12 <= i && 12U <= bound) && i <= 10000)) || (((11 <=
        i && 11U <= bound) && i <= 10000) && _he_bkt_i == 512U)) || (((7 <= i && 7U
        <= bound) && i <= 10000) && _he_bkt_i == 32U)) || (((10 <= i && 10U <= bound)
        && i <= 10000) && _he_bkt_i == 256U)) || (2U <= bound && i == 2)) || (3U <=
        bound && i == 3)) || (5U <= bound && i == 5)) || (4U <= bound && i == 4))
        || ((1U <= bound && i == 1) && user == users))) || ((((0 == i && 0 == users)
        && i == 0) && i == users) && 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_test2-2.i
        line: 826
        column: 216
        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_test2-2.i
        line: 826
        column: 216
        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_test2-2.i
        line: 826
        column: 216
        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_test2-2.i
        line: 826
        column: 216
        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_test2-2.i
        line: 826
        column: 216
        function: main
      value: 0xfeedbeefu == _hf_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_test2-2.i
        line: 826
        column: 216
        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_test2-2.i
        line: 826
        column: 216
        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_test2-2.i
        line: 826
        column: 216
        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_test2-2.i
        line: 826
        column: 216
        function: main
      value: _hf_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_test2-2.i
        line: 826
        column: 216
        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_test2-2.i
        line: 826
        column: 216
        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_test2-2.i
        line: 826
        column: 216
        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_test2-2.i
        line: 826
        column: 216
        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_test2-2.i
        line: 826
        column: 216
        function: main
      value: _hj_key == & 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_test2-2.i
        line: 826
        column: 216
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 826
        column: 216
        function: main
      value: (((((2 <= i && 2 <= *((int *)_hj_key)) && ((((((((i <= 9999 && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && (((8U <= bound && _he_bkt_i ==
        64U) || (9U <= bound && _he_bkt_i == 128U)) || 7U <= bound)) || ((i <= 5 &&
        *((int *)_hj_key) <= 5) && bound == 6U)) || (((12U <= bound && i <= 9999)
        && bound <= 10000U) && *((int *)_hj_key) <= 9999)) || ((((11U <= bound &&
        i <= 9999) && bound <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i
        == 512U)) || ((((7U <= bound && i <= 9999) && bound <= 10000U) && *((int *)_hj_key)
        <= 9999) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9999) && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i == 256U))) || ((i ==
        2 && bound == 3U) && *((int *)_hj_key) == 2)) || ((((2 <= i && 2 <= *((int
        *)_hj_key)) && i <= 4) && *((int *)_hj_key) <= 4) && bound == 5U)) || ((((2
        <= i && 2 <= *((int *)_hj_key)) && i <= 3) && *((int *)_hj_key) <= 3) && bound
        == 4U)) || (((0 == i && i == 0) && *((int *)_hj_key) == 0) && (((((((((((bound
        <= 10000U && (((8U <= bound && _he_bkt_i == 64U) || (9U <= bound && _he_bkt_i
        == 128U)) || 7U <= bound)) || bound == 6U) || (12U <= bound && bound <= 10000U))
        || ((11U <= bound && bound <= 10000U) && _he_bkt_i == 512U)) || ((7U <= bound
        && bound <= 10000U) && _he_bkt_i == 32U)) || ((10U <= bound && bound <= 10000U)
        && _he_bkt_i == 256U)) || bound == 2U) || bound == 3U) || bound == 5U) ||
        bound == 4U) || (user == users && bound == 1U)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i
        line: 826
        column: 2685
        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_test2-2.i
        line: 826
        column: 2685
        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_test2-2.i
        line: 826
        column: 2685
        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_test2-2.i
        line: 826
        column: 2685
        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_test2-2.i
        line: 826
        column: 2685
        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_test2-2.i
        line: 826
        column: 2685
        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_test2-2.i
        line: 826
        column: 2685
        function: main
      value: _hj_key == & 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_test2-2.i
        line: 826
        column: 2685
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 826
        column: 2685
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9999 && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && (((8U <= bound && _he_bkt_i ==
        64U) || (9U <= bound && _he_bkt_i == 128U)) || 7U <= bound)) || ((i <= 5 &&
        *((int *)_hj_key) <= 5) && bound == 6U)) || (((12U <= bound && i <= 9999)
        && bound <= 10000U) && *((int *)_hj_key) <= 9999)) || ((((11U <= bound &&
        i <= 9999) && bound <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i
        == 512U)) || ((((7U <= bound && i <= 9999) && bound <= 10000U) && *((int *)_hj_key)
        <= 9999) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9999) && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i == 256U))) || (((0 ==
        i && i == 0) && bound == 2U) && *((int *)_hj_key) == 0)) || ((((0 <= i &&
        0 <= *((int *)_hj_key)) && i <= 2) && *((int *)_hj_key) <= 2) && bound ==
        3U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key)
        <= 4) && bound == 5U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 3)
        && *((int *)_hj_key) <= 3) && bound == 4U)) || ((((0 == i && i == 0) && user
        == users) && bound == 1U) && *((int *)_hj_key) == 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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 3360
        function: main
      value: (((((((((i <= 9999 && ((((8 <= i && 9U <= bound) && _he_bkt_i == 64U)
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || (6 <= i && 7U <= bound)))
        || (6U <= bound && i == 5)) || ((12 <= i && 13U <= bound) && i <= 9999)) ||
        (((11 <= i && 12U <= bound) && i <= 9999) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9999) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9999) && _he_bkt_i == 256U)) || (2U <= bound && i == 1))
        || (3U <= bound && i == 2)) || (5U <= bound && i == 4)) || (4U <= bound &&
        i == 3)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i
        line: 830
        column: 5
        function: main
      value: ((((user == users && ((((((((((((((((((((((((((0 == i && 0 == user) &&
        0 == users) && 0 == temp) && i == 0) && i == user) && i == users) && i ==
        temp) && user == 0) && user == temp) && users == 0) && users == temp) && bound
        == 0U) && temp == 0) || (((((((((((((8 <= i && 8 <= *((int *)_hj_key)) &&
        8U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)
        && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 64U) && _hj_k == 4U) && _hj_key == & i) && (void *)_hj_key == (void *)(&
        i))) || (((((((((((((9 <= i && 9 <= *((int *)_hj_key)) && 9U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && 4UL == _hj_k)
        && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 128U)
        && _hj_k == 4U) && _hj_key == & i) && (void *)_hj_key == (void *)(& i))) ||
        ((((((((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && 4UL == _hj_k) && 4UL
        == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _hj_key ==
        & i) && (void *)_hj_key == (void *)(& i))) || (((((((((((6 <= i && 6 <= *((int
        *)_hj_key)) && i <= 7) && *((int *)_hj_key) <= 7) && 4UL == _hj_k) && 4UL
        == _hj_k) && bound == 6U) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U)
        && _hj_key == & i) && (void *)_hj_key == (void *)(& i))) || ((((((((((((12
        <= i && 12 <= *((int *)_hj_key)) && 12U <= bound) && i <= 10001) && bound
        <= 10000U) && *((int *)_hj_key) <= 10001) && 4UL == _hj_k) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _hj_key == & i) && (void
        *)_hj_key == (void *)(& i))) || (((((((((((((11 <= i && 11 <= *((int *)_hj_key))
        && 11U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _he_bkt_i == 512U) && _hj_k == 4U) && _hj_key == & i) && (void *)_hj_key
        == (void *)(& i))) || (((((((((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U
        <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)
        && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 32U) && _hj_k == 4U) && _hj_key == & i) && (void *)_hj_key == (void *)(&
        i))) || (((((((((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound)
        && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && 4UL ==
        _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i ==
        256U) && _hj_k == 4U) && _hj_key == & i) && (void *)_hj_key == (void *)(&
        i))) || (((((((((4UL == _hj_k && 4UL == _hj_k) && i == 2) && bound == 2U)
        && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _hj_key == & i) && *((int
        *)_hj_key) == 2) && (void *)_hj_key == (void *)(& i))) || (((((((((((3 <=
        i && 3 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key) <= 4) && 4UL
        == _hj_k) && 4UL == _hj_k) && bound == 3U) && _hj_k == 4U) && _hj_k == _hj_k)
        && _hj_k == 4U) && _hj_key == & i) && (void *)_hj_key == (void *)(& i))) ||
        (((((((((((5 <= i && 5 <= *((int *)_hj_key)) && i <= 6) && *((int *)_hj_key)
        <= 6) && 4UL == _hj_k) && 4UL == _hj_k) && bound == 5U) && _hj_k == 4U) &&
        _hj_k == _hj_k) && _hj_k == 4U) && _hj_key == & i) && (void *)_hj_key == (void
        *)(& i))) || (((((((((((4 <= i && 4 <= *((int *)_hj_key)) && i <= 5) && *((int
        *)_hj_key) <= 5) && 4UL == _hj_k) && 4UL == _hj_k) && bound == 4U) && _hj_k
        == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _hj_key == & i) && (void *)_hj_key
        == (void *)(& i))) || ((((((((((4UL == _hj_k && 4UL == _hj_k) && i == 2) &&
        bound == 1U) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && _hj_key
        == & i) && temp == 0) && *((int *)_hj_key) == 2) && (void *)_hj_key == (void
        *)(& i)))) || ((((((4UL == _hj_k && 4UL == _hj_k) && _hj_k == 4U) && _hj_k
        == _hj_k) && _hj_k == 4U) && (void *)_hj_key == (void *)(& i)) && ((((((((((((((((((((((((i
        <= 10001 && bound <= 10000U) && *((int *)_hj_key) <= 10001) && (((((8 <= i
        && 8 <= *((int *)_hj_key)) && 8U <= bound) && _he_bkt_i == 64U) || (((9 <=
        i && 9 <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U)) || (((9
        <= i && 9 <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U))) ||
        (((((6 <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int *)_hj_key) <=
        7) && bound == 6U) && temp == 0)) || (((((7 <= i && 7 <= *((int *)_hj_key))
        && 7U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001)) || (((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || ((((6 <= i &&
        6 <= *((int *)_hj_key)) && i <= 7) && *((int *)_hj_key) <= 7) && bound ==
        6U)) || (((((12 <= i && 12 <= *((int *)_hj_key)) && 12U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || (((((12 <= i
        && 12 <= *((int *)_hj_key)) && 12U <= bound) && i <= 10001) && bound <= 10000U)
        && *((int *)_hj_key) <= 10001)) || ((((((11 <= i && 11 <= *((int *)_hj_key))
        && 11U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001) && _he_bkt_i == 512U)) || ((((((11 <= i && 11 <= *((int *)_hj_key))
        && 11U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001) && _he_bkt_i == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) &&
        7U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)
        && _he_bkt_i == 32U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <=
        bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) &&
        _he_bkt_i == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <=
        bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) &&
        _he_bkt_i == 256U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <=
        bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) &&
        _he_bkt_i == 256U)) || ((((((8 <= i && 8 <= *((int *)_hj_key)) && 8U <= bound)
        && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 64U)) || ((((((9 <= i && 9 <= *((int *)_hj_key)) && 9U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i ==
        128U)) || ((((((((4 <= i && 4 <= *((int *)_hj_key)) && 4U <= bound) && i <=
        7) && bound <= 6U) && *((int *)_hj_key) <= 7) && 0 == temp) && user == 0)
        && temp == 0)) || (((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || (((((5
        <= i && 5 <= *((int *)_hj_key)) && i <= 6) && *((int *)_hj_key) <= 6) && bound
        == 5U) && temp == 0)) || (((((12 <= i && 12 <= *((int *)_hj_key)) && 12U <=
        bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001))
        || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 512U))
        || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 32U)) ||
        ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 256U))))
        || ((((((4UL == _hj_k && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _hj_k == 4U) && (void *)_hj_key == (void *)(& i)) && (((((((((((i <= 10001
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && (((((8 <= i && 8 <=
        *((int *)_hj_key)) && 8U <= bound) && _he_bkt_i == 64U) || (((9 <= i && 9
        <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i &&
        7 <= *((int *)_hj_key)) && 7U <= bound))) || ((((6 <= i && 6 <= *((int *)_hj_key))
        && i <= 7) && *((int *)_hj_key) <= 7) && bound == 6U)) || (((((12 <= i &&
        12 <= *((int *)_hj_key)) && 12U <= bound) && i <= 10001) && bound <= 10000U)
        && *((int *)_hj_key) <= 10001)) || ((((((11 <= i && 11 <= *((int *)_hj_key))
        && 11U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001) && _he_bkt_i == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) &&
        7U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)
        && _he_bkt_i == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U
        <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)
        && _he_bkt_i == 256U)) || (((((((3 <= i && 3 <= *((int *)_hj_key)) && i <=
        4) && *((int *)_hj_key) <= 4) && 0 == temp) && user == 0) && bound == 3U)
        && temp == 0)) || ((((5 <= i && 5 <= *((int *)_hj_key)) && i <= 6) && *((int
        *)_hj_key) <= 6) && bound == 5U)) || (((((4 <= i && 4 <= *((int *)_hj_key))
        && i <= 5) && *((int *)_hj_key) <= 5) && bound == 4U) && temp == 0)))) ||
        (((((((4UL == _hj_k && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) &&
        _hj_k == 4U) && _hj_key == & i) && (void *)_hj_key == (void *)(& i)) && ((((((((((((i
        <= 10001 && bound <= 10000U) && *((int *)_hj_key) <= 10001) && (((((8 <= i
        && 8 <= *((int *)_hj_key)) && 8U <= bound) && _he_bkt_i == 64U) || (((9 <=
        i && 9 <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U)) || ((7
        <= i && 7 <= *((int *)_hj_key)) && 7U <= bound))) || ((((6 <= i && 6 <= *((int
        *)_hj_key)) && i <= 7) && *((int *)_hj_key) <= 7) && bound == 6U)) || (((((12
        <= i && 12 <= *((int *)_hj_key)) && 12U <= bound) && i <= 10001) && bound
        <= 10000U) && *((int *)_hj_key) <= 10001)) || ((((((11 <= i && 11 <= *((int
        *)_hj_key)) && 11U <= bound) && i <= 10001) && bound <= 10000U) && *((int
        *)_hj_key) <= 10001) && _he_bkt_i == 512U)) || ((((((7 <= i && 7 <= *((int
        *)_hj_key)) && 7U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key)
        <= 10001) && _he_bkt_i == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key))
        && 10U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001) && _he_bkt_i == 256U)) || (((((0 == temp && i == 2) && user == 0) &&
        bound == 2U) && temp == 0) && *((int *)_hj_key) == 2)) || (((((3 <= i && 3
        <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key) <= 4) && bound == 3U)
        && temp == 0)) || ((((5 <= i && 5 <= *((int *)_hj_key)) && i <= 6) && *((int
        *)_hj_key) <= 6) && bound == 5U)) || ((((4 <= i && 4 <= *((int *)_hj_key))
        && i <= 5) && *((int *)_hj_key) <= 5) && bound == 4U)))) || (((((((4UL ==
        _hj_k && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U)
        && _hj_key == & i) && (void *)_hj_key == (void *)(& i)) && ((((((((((((((((((((0
        == users && 0 == temp) && i == 2) && user == 0) && users == 0) && users ==
        temp) && bound == 1U) && temp == 0) && *((int *)_hj_key) == 2) || ((((((8
        <= i && 8 <= *((int *)_hj_key)) && 8U <= bound) && i <= 10001) && bound <=
        10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 64U)) || ((((((9 <=
        i && 9 <= *((int *)_hj_key)) && 9U <= bound) && i <= 10001) && bound <= 10000U)
        && *((int *)_hj_key) <= 10001) && _he_bkt_i == 128U)) || (((((7 <= i && 7
        <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001) && bound <= 10000U) &&
        *((int *)_hj_key) <= 10001)) || ((((6 <= i && 6 <= *((int *)_hj_key)) && i
        <= 7) && *((int *)_hj_key) <= 7) && bound == 6U)) || (((((12 <= i && 12 <=
        *((int *)_hj_key)) && 12U <= bound) && i <= 10001) && bound <= 10000U) &&
        *((int *)_hj_key) <= 10001)) || ((((((11 <= i && 11 <= *((int *)_hj_key))
        && 11U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001) && _he_bkt_i == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) &&
        7U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)
        && _he_bkt_i == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U
        <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)
        && _he_bkt_i == 256U)) || (((i == 2 && bound == 2U) && temp == 0) && *((int
        *)_hj_key) == 2)) || ((((3 <= i && 3 <= *((int *)_hj_key)) && i <= 4) && *((int
        *)_hj_key) <= 4) && bound == 3U)) || ((((5 <= i && 5 <= *((int *)_hj_key))
        && i <= 6) && *((int *)_hj_key) <= 6) && bound == 5U)) || ((((4 <= i && 4
        <= *((int *)_hj_key)) && i <= 5) && *((int *)_hj_key) <= 5) && bound == 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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 2467
        function: main
      value: ((((((((((i <= 9999 && ((((8 <= i && 9U <= bound) && _he_bkt_i == 64U)
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || (6 <= i && 7U <= bound)))
        || (6U <= bound && i == 5)) || ((12 <= i && 13U <= bound) && i <= 9999)) ||
        (((11 <= i && 12U <= bound) && i <= 9999) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9999) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9999) && _he_bkt_i == 256U)) || (2U <= bound && i == 1))
        || (3U <= bound && i == 2)) || (5U <= bound && i == 4)) || (4U <= bound &&
        i == 3)) || (((((1U <= bound && 0 == i) && 0 == users) && i == 0) && i ==
        users) && 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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 4976
        function: main
      value: (((((((8 <= i && 9U <= bound) && _he_bkt_i <= 127U) || ((7 <= i && 8U
        <= bound) && _he_bkt_i <= 63U)) || ((9 <= i && 10U <= bound) && _he_bkt_i
        <= 255U)) || ((6 <= i && 7U <= bound) && _he_bkt_i <= 31U)) || ((11 <= i &&
        12U <= bound) && _he_bkt_i <= 1023U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        <= 4294967294U)) || ((10 <= i && 11U <= bound) && _he_bkt_i <= 511U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i
        line: 826
        column: 1821
        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_test2-2.i
        line: 826
        column: 1821
        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_test2-2.i
        line: 826
        column: 1821
        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_test2-2.i
        line: 826
        column: 1821
        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_test2-2.i
        line: 826
        column: 1821
        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_test2-2.i
        line: 826
        column: 1821
        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_test2-2.i
        line: 826
        column: 1821
        function: main
      value: _hf_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_test2-2.i
        line: 826
        column: 1821
        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_test2-2.i
        line: 826
        column: 1821
        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_test2-2.i
        line: 826
        column: 1821
        function: main
      value: _hj_key == & 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_test2-2.i
        line: 826
        column: 1821
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 826
        column: 1821
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9999 && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && (((8U <= bound && _he_bkt_i ==
        64U) || (9U <= bound && _he_bkt_i == 128U)) || 7U <= bound)) || ((i <= 5 &&
        *((int *)_hj_key) <= 5) && bound == 6U)) || (((12U <= bound && i <= 9999)
        && bound <= 10000U) && *((int *)_hj_key) <= 9999)) || ((((11U <= bound &&
        i <= 9999) && bound <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i
        == 512U)) || ((((7U <= bound && i <= 9999) && bound <= 10000U) && *((int *)_hj_key)
        <= 9999) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9999) && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i == 256U))) || (((0 ==
        i && i == 0) && bound == 2U) && *((int *)_hj_key) == 0)) || ((((0 <= i &&
        0 <= *((int *)_hj_key)) && i <= 2) && *((int *)_hj_key) <= 2) && bound ==
        3U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key)
        <= 4) && bound == 5U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 3)
        && *((int *)_hj_key) <= 3) && bound == 4U)) || ((((0 == i && i == 0) && user
        == users) && bound == 1U) && *((int *)_hj_key) == 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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 1832
        function: main
      value: ((((((((((i <= 9999 && ((((8 <= i && 9U <= bound) && _he_bkt_i == 64U)
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || (6 <= i && 7U <= bound)))
        || (6U <= bound && i == 5)) || ((12 <= i && 13U <= bound) && i <= 9999)) ||
        (((11 <= i && 12U <= bound) && i <= 9999) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9999) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9999) && _he_bkt_i == 256U)) || (2U <= bound && i == 1))
        || (3U <= bound && i == 2)) || (5U <= bound && i == 4)) || (4U <= bound &&
        i == 3)) || (((((1U <= bound && 0 == i) && 0 == users) && i == 0) && i ==
        users) && 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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 3578
        function: main
      value: ((((((((((i <= 9999 && ((((8 <= i && 9U <= bound) && _he_bkt_i == 64U)
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || (6 <= i && 7U <= bound)))
        || (6U <= bound && i == 5)) || ((12 <= i && 13U <= bound) && i <= 9999)) ||
        (((11 <= i && 12U <= bound) && i <= 9999) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9999) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9999) && _he_bkt_i == 256U)) || (2U <= bound && i == 1))
        || (3U <= bound && i == 2)) || (5U <= bound && i == 4)) || (4U <= bound &&
        i == 3)) || (((1U <= bound && 0 == i) && i == 0) && 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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 4912
        function: main
      value: (((((((8 <= i && 9U <= bound) && _he_bkt_i <= 127U) || ((7 <= i && 8U
        <= bound) && _he_bkt_i <= 63U)) || ((9 <= i && 10U <= bound) && _he_bkt_i
        <= 255U)) || ((6 <= i && 7U <= bound) && _he_bkt_i <= 31U)) || ((11 <= i &&
        12U <= bound) && _he_bkt_i <= 1023U)) || ((12 <= i && 13U <= bound) && _he_bkt_i
        <= 4294967294U)) || ((10 <= i && 11U <= bound) && _he_bkt_i <= 511U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i
        line: 826
        column: 2856
        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_test2-2.i
        line: 826
        column: 2856
        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_test2-2.i
        line: 826
        column: 2856
        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_test2-2.i
        line: 826
        column: 2856
        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_test2-2.i
        line: 826
        column: 2856
        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_test2-2.i
        line: 826
        column: 2856
        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_test2-2.i
        line: 826
        column: 2856
        function: main
      value: _hj_key == & 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_test2-2.i
        line: 826
        column: 2856
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 826
        column: 2856
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9999 && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && (((8U <= bound && _he_bkt_i ==
        64U) || (9U <= bound && _he_bkt_i == 128U)) || 7U <= bound)) || ((i <= 5 &&
        *((int *)_hj_key) <= 5) && bound == 6U)) || (((12U <= bound && i <= 9999)
        && bound <= 10000U) && *((int *)_hj_key) <= 9999)) || ((((11U <= bound &&
        i <= 9999) && bound <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i
        == 512U)) || ((((7U <= bound && i <= 9999) && bound <= 10000U) && *((int *)_hj_key)
        <= 9999) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9999) && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i == 256U))) || (((0 ==
        i && i == 0) && bound == 2U) && *((int *)_hj_key) == 0)) || ((((0 <= i &&
        0 <= *((int *)_hj_key)) && i <= 2) && *((int *)_hj_key) <= 2) && bound ==
        3U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key)
        <= 4) && bound == 5U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 3)
        && *((int *)_hj_key) <= 3) && bound == 4U)) || ((((0 == i && i == 0) && user
        == users) && bound == 1U) && *((int *)_hj_key) == 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_test2-2.i
        line: 826
        column: 2456
        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_test2-2.i
        line: 826
        column: 2456
        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_test2-2.i
        line: 826
        column: 2456
        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_test2-2.i
        line: 826
        column: 2456
        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_test2-2.i
        line: 826
        column: 2456
        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_test2-2.i
        line: 826
        column: 2456
        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_test2-2.i
        line: 826
        column: 2456
        function: main
      value: _hj_key == & 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_test2-2.i
        line: 826
        column: 2456
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 826
        column: 2456
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9999 && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && (((8U <= bound && _he_bkt_i ==
        64U) || (9U <= bound && _he_bkt_i == 128U)) || 7U <= bound)) || ((i <= 5 &&
        *((int *)_hj_key) <= 5) && bound == 6U)) || (((12U <= bound && i <= 9999)
        && bound <= 10000U) && *((int *)_hj_key) <= 9999)) || ((((11U <= bound &&
        i <= 9999) && bound <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i
        == 512U)) || ((((7U <= bound && i <= 9999) && bound <= 10000U) && *((int *)_hj_key)
        <= 9999) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9999) && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i == 256U))) || (((0 ==
        i && i == 0) && bound == 2U) && *((int *)_hj_key) == 0)) || ((((0 <= i &&
        0 <= *((int *)_hj_key)) && i <= 2) && *((int *)_hj_key) <= 2) && bound ==
        3U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key)
        <= 4) && bound == 5U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 3)
        && *((int *)_hj_key) <= 3) && bound == 4U)) || ((((0 == i && i == 0) && user
        == users) && bound == 1U) && *((int *)_hj_key) == 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_test2-2.i
        line: 825
        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 == & i) && (void *)_hj_key
        == (void *)(& i)) && (((((((2 <= i && 2 <= *((int *)_hj_key)) && ((((((((i
        <= 10001 && bound <= 10000U) && *((int *)_hj_key) <= 10001) && (((8U <= bound
        && _he_bkt_i == 64U) || (9U <= bound && _he_bkt_i == 128U)) || 7U <= bound))
        || ((i <= 7 && *((int *)_hj_key) <= 7) && bound == 6U)) || (((12U <= bound
        && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || ((((11U
        <= bound && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)
        && _he_bkt_i == 512U)) || ((((7U <= bound && i <= 10001) && bound <= 10000U)
        && *((int *)_hj_key) <= 10001) && _he_bkt_i == 32U)) || ((((10U <= bound &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 256U))) || ((i == 2 && bound == 2U) && *((int *)_hj_key) == 2)) || ((((2
        <= i && 2 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key) <= 4) && bound
        == 3U)) || ((((2 <= i && 2 <= *((int *)_hj_key)) && i <= 6) && *((int *)_hj_key)
        <= 6) && bound == 5U)) || ((((2 <= i && 2 <= *((int *)_hj_key)) && i <= 5)
        && *((int *)_hj_key) <= 5) && bound == 4U)) || (((i == 2 && user == users)
        && bound == 1U) && *((int *)_hj_key) == 2))) || ((0 == i && i == 0) && ((((((((((((((((0
        == users && i == users) && users == 0) && bound == 0U) || (((((8U <= bound
        && bound <= 10000U) && 4UL == _hj_k) && _hj_k == 4U) && _hj_key == & user->id)
        && _he_bkt_i == 64U)) || (((((9U <= bound && bound <= 10000U) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_key == & user->id) && _he_bkt_i == 128U)) || ((((7U
        <= bound && bound <= 10000U) && 4UL == _hj_k) && _hj_k == 4U) && _hj_key ==
        & user->id)) || (((4UL == _hj_k && bound == 6U) && _hj_k == 4U) && _hj_key
        == & user->id)) || ((((12U <= bound && bound <= 10000U) && 4UL == _hj_k) &&
        _hj_k == 4U) && _hj_key == & user->id)) || (((((11U <= bound && bound <= 10000U)
        && 4UL == _hj_k) && _hj_k == 4U) && _hj_key == & user->id) && _he_bkt_i ==
        512U)) || (((((7U <= bound && bound <= 10000U) && 4UL == _hj_k) && _hj_k ==
        4U) && _hj_key == & user->id) && _he_bkt_i == 32U)) || (((((10U <= bound &&
        bound <= 10000U) && 4UL == _hj_k) && _hj_k == 4U) && _hj_key == & user->id)
        && _he_bkt_i == 256U)) || (((4UL == _hj_k && bound == 2U) && _hj_k == 4U)
        && _hj_key == & user->id)) || (((4UL == _hj_k && bound == 3U) && _hj_k ==
        4U) && _hj_key == & user->id)) || (((4UL == _hj_k && bound == 5U) && _hj_k
        == 4U) && _hj_key == & user->id)) || (((4UL == _hj_k && bound == 4U) && _hj_k
        == 4U) && _hj_key == & user->id)) || ((((4UL == _hj_k && user == users) &&
        bound == 1U) && _hj_k == 4U) && _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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 3631
        function: main
      value: ((((((((((i <= 9999 && ((((8 <= i && 9U <= bound) && _he_bkt_i == 64U)
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || (6 <= i && 7U <= bound)))
        || (6U <= bound && i == 5)) || ((12 <= i && 13U <= bound) && i <= 9999)) ||
        (((11 <= i && 12U <= bound) && i <= 9999) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9999) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9999) && _he_bkt_i == 256U)) || (2U <= bound && i == 1))
        || (3U <= bound && i == 2)) || (5U <= bound && i == 4)) || (4U <= bound &&
        i == 3)) || (((1U <= bound && 0 == i) && i == 0) && 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_test2-2.i
        line: 831
        column: 546
        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_test2-2.i
        line: 831
        column: 546
        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_test2-2.i
        line: 831
        column: 546
        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_test2-2.i
        line: 831
        column: 546
        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_test2-2.i
        line: 831
        column: 546
        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_test2-2.i
        line: 831
        column: 546
        function: main
      value: _hd_hh_del == & user->hh
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i
        line: 831
        column: 546
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 831
        column: 546
        function: main
      value: ((user == users && _hj_key == & i) && ((((((((((((i <= 10001 && bound
        <= 10000U) && *((int *)_hj_key) <= 10001) && (((((8 <= i && 8 <= *((int *)_hj_key))
        && 8U <= bound) && _he_bkt_i == 64U) || (((9 <= i && 9 <= *((int *)_hj_key))
        && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 7 <= *((int *)_hj_key))
        && 7U <= bound))) || ((((6 <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int
        *)_hj_key) <= 7) && bound == 6U)) || (((((12 <= i && 12 <= *((int *)_hj_key))
        && 12U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001)) || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 256U)) || ((i == 2 && bound == 2U) && *((int *)_hj_key) == 2)) || ((((3
        <= i && 3 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key) <= 4) && bound
        == 3U)) || ((((5 <= i && 5 <= *((int *)_hj_key)) && i <= 6) && *((int *)_hj_key)
        <= 6) && bound == 5U)) || ((((4 <= i && 4 <= *((int *)_hj_key)) && i <= 5)
        && *((int *)_hj_key) <= 5) && bound == 4U))) || (((i <= 10001 && bound <=
        10000U) && *((int *)_hj_key) <= 10001) && (((((((((8 <= i && 8 <= *((int *)_hj_key))
        && 8U <= bound) && _he_bkt_i == 64U) || (((9 <= i && 9 <= *((int *)_hj_key))
        && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 7 <= *((int *)_hj_key))
        && 7U <= bound)) || ((12 <= i && 12 <= *((int *)_hj_key)) && 12U <= bound))
        || (((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && _he_bkt_i ==
        512U)) || (((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && _he_bkt_i
        == 32U)) || (((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && _he_bkt_i
        == 256U)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 3714
        function: main
      value: ((((((((((i <= 9999 && ((((8 <= i && 9U <= bound) && _he_bkt_i == 64U)
        || ((9 <= i && 10U <= bound) && _he_bkt_i == 128U)) || (6 <= i && 7U <= bound)))
        || (6U <= bound && i == 5)) || ((12 <= i && 13U <= bound) && i <= 9999)) ||
        (((11 <= i && 12U <= bound) && i <= 9999) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9999) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9999) && _he_bkt_i == 256U)) || (2U <= bound && i == 1))
        || (3U <= bound && i == 2)) || (5U <= bound && i == 4)) || (4U <= bound &&
        i == 3)) || (((1U <= bound && 0 == i) && i == 0) && 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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        column: 39
        function: main
      value: ((4UL == _hj_k && _hj_k == 4U) && ((((((((((i <= 9999 && ((((8 <= i &&
        9U <= bound) && _he_bkt_i == 64U) || ((9 <= i && 10U <= bound) && _he_bkt_i
        == 128U)) || (6 <= i && 7U <= bound))) || (6U <= bound && i == 5)) || ((12
        <= i && 13U <= bound) && i <= 9999)) || (((11 <= i && 12U <= bound) && i <=
        9999) && _he_bkt_i == 512U)) || (((7 <= i && 8U <= bound) && i <= 9999) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && i <= 9999) && _he_bkt_i
        == 256U)) || (2U <= bound && i == 1)) || (3U <= bound && i == 2)) || (5U <=
        bound && i == 4)) || (4U <= bound && i == 3))) || (((((1U <= bound && 0 ==
        i) && 0 == users) && i == 0) && i == users) && 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_test2-2.i
        line: 826
        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_test2-2.i
        line: 826
        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_test2-2.i
        line: 826
        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_test2-2.i
        line: 826
        column: 39
        function: main
      value: (((((4UL == _hj_k && _hj_k == _hj_k) && _hj_k == 4U) && _hj_key == &
        i) && (void *)_hj_key == (void *)(& i)) && (((((2 <= i && 2 <= *((int *)_hj_key))
        && ((((((((i <= 9999 && bound <= 10000U) && *((int *)_hj_key) <= 9999) &&
        (((8U <= bound && _he_bkt_i == 64U) || (9U <= bound && _he_bkt_i == 128U))
        || 7U <= bound)) || ((i <= 5 && *((int *)_hj_key) <= 5) && bound == 6U)) ||
        (((12U <= bound && i <= 9999) && bound <= 10000U) && *((int *)_hj_key) <=
        9999)) || ((((11U <= bound && i <= 9999) && bound <= 10000U) && *((int *)_hj_key)
        <= 9999) && _he_bkt_i == 512U)) || ((((7U <= bound && i <= 9999) && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i == 32U)) || ((((10U
        <= bound && i <= 9999) && bound <= 10000U) && *((int *)_hj_key) <= 9999) &&
        _he_bkt_i == 256U))) || ((i == 2 && bound == 3U) && *((int *)_hj_key) == 2))
        || ((((2 <= i && 2 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key) <=
        4) && bound == 5U)) || ((((2 <= i && 2 <= *((int *)_hj_key)) && i <= 3) &&
        *((int *)_hj_key) <= 3) && bound == 4U))) || ((0 == i && i == 0) && (((((((((((bound
        <= 10000U && (((8U <= bound && _he_bkt_i == 64U) || (9U <= bound && _he_bkt_i
        == 128U)) || 7U <= bound)) || bound == 6U) || (12U <= bound && bound <= 10000U))
        || ((11U <= bound && bound <= 10000U) && _he_bkt_i == 512U)) || ((7U <= bound
        && bound <= 10000U) && _he_bkt_i == 32U)) || ((10U <= bound && bound <= 10000U)
        && _he_bkt_i == 256U)) || bound == 2U) || bound == 3U) || bound == 5U) ||
        bound == 4U) || (user == users && bound == 1U)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i
        line: 826
        column: 2513
        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_test2-2.i
        line: 826
        column: 2513
        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_test2-2.i
        line: 826
        column: 2513
        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_test2-2.i
        line: 826
        column: 2513
        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_test2-2.i
        line: 826
        column: 2513
        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_test2-2.i
        line: 826
        column: 2513
        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_test2-2.i
        line: 826
        column: 2513
        function: main
      value: _hj_key == & 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_test2-2.i
        line: 826
        column: 2513
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 826
        column: 2513
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9999 && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && (((8U <= bound && _he_bkt_i ==
        64U) || (9U <= bound && _he_bkt_i == 128U)) || 7U <= bound)) || ((i <= 5 &&
        *((int *)_hj_key) <= 5) && bound == 6U)) || (((12U <= bound && i <= 9999)
        && bound <= 10000U) && *((int *)_hj_key) <= 9999)) || ((((11U <= bound &&
        i <= 9999) && bound <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i
        == 512U)) || ((((7U <= bound && i <= 9999) && bound <= 10000U) && *((int *)_hj_key)
        <= 9999) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9999) && bound
        <= 10000U) && *((int *)_hj_key) <= 9999) && _he_bkt_i == 256U))) || (((0 ==
        i && i == 0) && bound == 2U) && *((int *)_hj_key) == 0)) || ((((0 <= i &&
        0 <= *((int *)_hj_key)) && i <= 2) && *((int *)_hj_key) <= 2) && bound ==
        3U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key)
        <= 4) && bound == 5U)) || ((((0 <= i && 0 <= *((int *)_hj_key)) && i <= 3)
        && *((int *)_hj_key) <= 3) && bound == 4U)) || ((((0 == i && i == 0) && user
        == users) && bound == 1U) && *((int *)_hj_key) == 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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 823
        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_test2-2.i
        line: 831
        column: 848
        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_test2-2.i
        line: 831
        column: 848
        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_test2-2.i
        line: 831
        column: 848
        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_test2-2.i
        line: 831
        column: 848
        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_test2-2.i
        line: 831
        column: 848
        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_test2-2.i
        line: 831
        column: 848
        function: main
      value: _hd_hh_del == & user->hh
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_nondet_test2-2.i
        line: 831
        column: 848
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 831
        column: 848
        function: main
      value: ((((_hj_key == & i && ((((((((((((i <= 10001 && bound <= 10000U) && *((int
        *)_hj_key) <= 10001) && (((((8 <= i && 8 <= *((int *)_hj_key)) && 8U <= bound)
        && _he_bkt_i == 64U) || (((9 <= i && 9 <= *((int *)_hj_key)) && 9U <= bound)
        && _he_bkt_i == 128U)) || ((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound)))
        || ((((6 <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int *)_hj_key) <=
        7) && bound == 6U)) || (((((12 <= i && 12 <= *((int *)_hj_key)) && 12U <=
        bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001))
        || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 512U))
        || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 32U)) ||
        ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 256U))
        || ((i == 2 && bound == 2U) && *((int *)_hj_key) == 2)) || ((((3 <= i && 3
        <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key) <= 4) && bound == 3U))
        || ((((5 <= i && 5 <= *((int *)_hj_key)) && i <= 6) && *((int *)_hj_key) <=
        6) && bound == 5U)) || ((((4 <= i && 4 <= *((int *)_hj_key)) && i <= 5) &&
        *((int *)_hj_key) <= 5) && bound == 4U))) || (((((((((((((((((((((((i <= 10001
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && (((((8 <= i && 8 <=
        *((int *)_hj_key)) && 8U <= bound) && _he_bkt_i == 64U) || (((9 <= i && 9
        <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U)) || (((9 <= i
        && 9 <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U))) || (((((6
        <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int *)_hj_key) <= 7) && bound
        == 6U) && temp == 0)) || (((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound)
        && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || (((((7
        <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001) && bound <=
        10000U) && *((int *)_hj_key) <= 10001)) || ((((6 <= i && 6 <= *((int *)_hj_key))
        && i <= 7) && *((int *)_hj_key) <= 7) && bound == 6U)) || (((((12 <= i &&
        12 <= *((int *)_hj_key)) && 12U <= bound) && i <= 10001) && bound <= 10000U)
        && *((int *)_hj_key) <= 10001)) || (((((12 <= i && 12 <= *((int *)_hj_key))
        && 12U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001)) || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 512U)) || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 32U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i ==
        32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i ==
        256U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 256U)) || ((((((8 <= i && 8 <= *((int *)_hj_key)) && 8U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 64U)) || ((((((9 <= i && 9 <= *((int *)_hj_key)) && 9U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i ==
        128U)) || (((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || (((((5 <= i && 5 <=
        *((int *)_hj_key)) && i <= 6) && *((int *)_hj_key) <= 6) && bound == 5U) &&
        temp == 0)) || (((((12 <= i && 12 <= *((int *)_hj_key)) && 12U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || ((((((11
        <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i <= 10001) && bound
        <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 512U)) || ((((((7
        <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001) && bound <=
        10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 32U)) || ((((((10 <=
        i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <= 10001) && bound <=
        10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 256U))) || ((((((((((i
        <= 10001 && bound <= 10000U) && *((int *)_hj_key) <= 10001) && (((((8 <= i
        && 8 <= *((int *)_hj_key)) && 8U <= bound) && _he_bkt_i == 64U) || (((9 <=
        i && 9 <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U)) || ((7
        <= i && 7 <= *((int *)_hj_key)) && 7U <= bound))) || ((((6 <= i && 6 <= *((int
        *)_hj_key)) && i <= 7) && *((int *)_hj_key) <= 7) && bound == 6U)) || (((((12
        <= i && 12 <= *((int *)_hj_key)) && 12U <= bound) && i <= 10001) && bound
        <= 10000U) && *((int *)_hj_key) <= 10001)) || ((((((11 <= i && 11 <= *((int
        *)_hj_key)) && 11U <= bound) && i <= 10001) && bound <= 10000U) && *((int
        *)_hj_key) <= 10001) && _he_bkt_i == 512U)) || ((((((7 <= i && 7 <= *((int
        *)_hj_key)) && 7U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key)
        <= 10001) && _he_bkt_i == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key))
        && 10U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001) && _he_bkt_i == 256U)) || ((((5 <= i && 5 <= *((int *)_hj_key)) &&
        i <= 6) && *((int *)_hj_key) <= 6) && bound == 5U)) || (((((4 <= i && 4 <=
        *((int *)_hj_key)) && i <= 5) && *((int *)_hj_key) <= 5) && bound == 4U) &&
        temp == 0))) || (_hj_key == & i && (((((((((((i <= 10001 && bound <= 10000U)
        && *((int *)_hj_key) <= 10001) && (((((8 <= i && 8 <= *((int *)_hj_key)) &&
        8U <= bound) && _he_bkt_i == 64U) || (((9 <= i && 9 <= *((int *)_hj_key))
        && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 7 <= *((int *)_hj_key))
        && 7U <= bound))) || ((((6 <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int
        *)_hj_key) <= 7) && bound == 6U)) || (((((12 <= i && 12 <= *((int *)_hj_key))
        && 12U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001)) || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 256U)) || (((((3 <= i && 3 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key)
        <= 4) && bound == 3U) && temp == 0)) || ((((5 <= i && 5 <= *((int *)_hj_key))
        && i <= 6) && *((int *)_hj_key) <= 6) && bound == 5U)) || ((((4 <= i && 4
        <= *((int *)_hj_key)) && i <= 5) && *((int *)_hj_key) <= 5) && bound == 4U))))
        || (_hj_key == & i && ((((((((((((i <= 10001 && bound <= 10000U) && *((int
        *)_hj_key) <= 10001) && (((((8 <= i && 8 <= *((int *)_hj_key)) && 8U <= bound)
        && _he_bkt_i == 64U) || (((9 <= i && 9 <= *((int *)_hj_key)) && 9U <= bound)
        && _he_bkt_i == 128U)) || ((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound)))
        || ((((6 <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int *)_hj_key) <=
        7) && bound == 6U)) || (((((12 <= i && 12 <= *((int *)_hj_key)) && 12U <=
        bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001))
        || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 512U))
        || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 32U)) ||
        ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 256U))
        || (((i == 2 && bound == 2U) && temp == 0) && *((int *)_hj_key) == 2)) ||
        ((((3 <= i && 3 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key) <= 4)
        && bound == 3U)) || ((((5 <= i && 5 <= *((int *)_hj_key)) && i <= 6) && *((int
        *)_hj_key) <= 6) && bound == 5U)) || ((((4 <= i && 4 <= *((int *)_hj_key))
        && i <= 5) && *((int *)_hj_key) <= 5) && bound == 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_test2-2.i
        line: 831
        column: 7
        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_test2-2.i
        line: 831
        column: 7
        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_test2-2.i
        line: 831
        column: 7
        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_test2-2.i
        line: 831
        column: 7
        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_test2-2.i
        line: 831
        column: 7
        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_test2-2.i
        line: 831
        column: 7
        function: main
      value: (void *)_hj_key == (void *)(& 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_test2-2.i
        line: 831
        column: 7
        function: main
      value: (((((user == users && _hj_key == & i) && (((((((((((((i <= 10001 && bound
        <= 10000U) && *((int *)_hj_key) <= 10001) && (((((8 <= i && 8 <= *((int *)_hj_key))
        && 8U <= bound) && _he_bkt_i == 64U) || (((9 <= i && 9 <= *((int *)_hj_key))
        && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 7 <= *((int *)_hj_key))
        && 7U <= bound))) || ((((6 <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int
        *)_hj_key) <= 7) && bound == 6U)) || (((((12 <= i && 12 <= *((int *)_hj_key))
        && 12U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001)) || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 256U)) || ((i == 2 && bound == 2U) && *((int *)_hj_key) == 2)) || ((((3
        <= i && 3 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key) <= 4) && bound
        == 3U)) || ((((5 <= i && 5 <= *((int *)_hj_key)) && i <= 6) && *((int *)_hj_key)
        <= 6) && bound == 5U)) || ((((4 <= i && 4 <= *((int *)_hj_key)) && i <= 5)
        && *((int *)_hj_key) <= 5) && bound == 4U)) || (((i == 2 && bound == 1U) &&
        temp == 0) && *((int *)_hj_key) == 2))) || (((((((((((((((((((((((i <= 10001
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && (((((8 <= i && 8 <=
        *((int *)_hj_key)) && 8U <= bound) && _he_bkt_i == 64U) || (((9 <= i && 9
        <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U)) || (((9 <= i
        && 9 <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U))) || (((((6
        <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int *)_hj_key) <= 7) && bound
        == 6U) && temp == 0)) || (((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound)
        && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || (((((7
        <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001) && bound <=
        10000U) && *((int *)_hj_key) <= 10001)) || ((((6 <= i && 6 <= *((int *)_hj_key))
        && i <= 7) && *((int *)_hj_key) <= 7) && bound == 6U)) || (((((12 <= i &&
        12 <= *((int *)_hj_key)) && 12U <= bound) && i <= 10001) && bound <= 10000U)
        && *((int *)_hj_key) <= 10001)) || (((((12 <= i && 12 <= *((int *)_hj_key))
        && 12U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001)) || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 512U)) || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 32U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i ==
        32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i ==
        256U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 256U)) || ((((((8 <= i && 8 <= *((int *)_hj_key)) && 8U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 64U)) || ((((((9 <= i && 9 <= *((int *)_hj_key)) && 9U <= bound) && i <=
        10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i ==
        128U)) || (((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || (((((5 <= i && 5 <=
        *((int *)_hj_key)) && i <= 6) && *((int *)_hj_key) <= 6) && bound == 5U) &&
        temp == 0)) || (((((12 <= i && 12 <= *((int *)_hj_key)) && 12U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001)) || ((((((11
        <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i <= 10001) && bound
        <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 512U)) || ((((((7
        <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001) && bound <=
        10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 32U)) || ((((((10 <=
        i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <= 10001) && bound <=
        10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 256U))) || ((((((((((i
        <= 10001 && bound <= 10000U) && *((int *)_hj_key) <= 10001) && (((((8 <= i
        && 8 <= *((int *)_hj_key)) && 8U <= bound) && _he_bkt_i == 64U) || (((9 <=
        i && 9 <= *((int *)_hj_key)) && 9U <= bound) && _he_bkt_i == 128U)) || ((7
        <= i && 7 <= *((int *)_hj_key)) && 7U <= bound))) || ((((6 <= i && 6 <= *((int
        *)_hj_key)) && i <= 7) && *((int *)_hj_key) <= 7) && bound == 6U)) || (((((12
        <= i && 12 <= *((int *)_hj_key)) && 12U <= bound) && i <= 10001) && bound
        <= 10000U) && *((int *)_hj_key) <= 10001)) || ((((((11 <= i && 11 <= *((int
        *)_hj_key)) && 11U <= bound) && i <= 10001) && bound <= 10000U) && *((int
        *)_hj_key) <= 10001) && _he_bkt_i == 512U)) || ((((((7 <= i && 7 <= *((int
        *)_hj_key)) && 7U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key)
        <= 10001) && _he_bkt_i == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key))
        && 10U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001) && _he_bkt_i == 256U)) || ((((5 <= i && 5 <= *((int *)_hj_key)) &&
        i <= 6) && *((int *)_hj_key) <= 6) && bound == 5U)) || (((((4 <= i && 4 <=
        *((int *)_hj_key)) && i <= 5) && *((int *)_hj_key) <= 5) && bound == 4U) &&
        temp == 0))) || (_hj_key == & i && (((((((((((i <= 10001 && bound <= 10000U)
        && *((int *)_hj_key) <= 10001) && (((((8 <= i && 8 <= *((int *)_hj_key)) &&
        8U <= bound) && _he_bkt_i == 64U) || (((9 <= i && 9 <= *((int *)_hj_key))
        && 9U <= bound) && _he_bkt_i == 128U)) || ((7 <= i && 7 <= *((int *)_hj_key))
        && 7U <= bound))) || ((((6 <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int
        *)_hj_key) <= 7) && bound == 6U)) || (((((12 <= i && 12 <= *((int *)_hj_key))
        && 12U <= bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <=
        10001)) || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i
        <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) &&
        i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i
        == 256U)) || (((((3 <= i && 3 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key)
        <= 4) && bound == 3U) && temp == 0)) || ((((5 <= i && 5 <= *((int *)_hj_key))
        && i <= 6) && *((int *)_hj_key) <= 6) && bound == 5U)) || ((((4 <= i && 4
        <= *((int *)_hj_key)) && i <= 5) && *((int *)_hj_key) <= 5) && bound == 4U))))
        || (_hj_key == & i && ((((((((((((i <= 10001 && bound <= 10000U) && *((int
        *)_hj_key) <= 10001) && (((((8 <= i && 8 <= *((int *)_hj_key)) && 8U <= bound)
        && _he_bkt_i == 64U) || (((9 <= i && 9 <= *((int *)_hj_key)) && 9U <= bound)
        && _he_bkt_i == 128U)) || ((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound)))
        || ((((6 <= i && 6 <= *((int *)_hj_key)) && i <= 7) && *((int *)_hj_key) <=
        7) && bound == 6U)) || (((((12 <= i && 12 <= *((int *)_hj_key)) && 12U <=
        bound) && i <= 10001) && bound <= 10000U) && *((int *)_hj_key) <= 10001))
        || ((((((11 <= i && 11 <= *((int *)_hj_key)) && 11U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 512U))
        || ((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 32U)) ||
        ((((((10 <= i && 10 <= *((int *)_hj_key)) && 10U <= bound) && i <= 10001)
        && bound <= 10000U) && *((int *)_hj_key) <= 10001) && _he_bkt_i == 256U))
        || (((i == 2 && bound == 2U) && temp == 0) && *((int *)_hj_key) == 2)) ||
        ((((3 <= i && 3 <= *((int *)_hj_key)) && i <= 4) && *((int *)_hj_key) <= 4)
        && bound == 3U)) || ((((5 <= i && 5 <= *((int *)_hj_key)) && i <= 6) && *((int
        *)_hj_key) <= 6) && bound == 5U)) || ((((4 <= i && 4 <= *((int *)_hj_key))
        && i <= 5) && *((int *)_hj_key) <= 5) && bound == 4U)))
      format: c_expression
