- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 83b4b097-feb2-433f-8041-ad361810dce4
    creation_time: 2025-03-22T09:51:55Z
    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_SFH_nondet_test3-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i: 6fd297418200393a9bb890e84311a80b6eacd7d5d7cdd65efb1397f8b8ab870f
      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_SFH_nondet_test3-1.i
        line: 750
        column: 853
        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_SFH_nondet_test3-1.i
        line: 750
        column: 853
        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_SFH_nondet_test3-1.i
        line: 750
        column: 853
        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_SFH_nondet_test3-1.i
        line: 750
        column: 853
        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_SFH_nondet_test3-1.i
        line: 750
        column: 853
        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_SFH_nondet_test3-1.i
        line: 750
        column: 853
        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_SFH_nondet_test3-1.i
        line: 750
        column: 853
        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_SFH_nondet_test3-1.i
        line: 750
        column: 853
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i == 256U))) || ((((0 ==
        i && i == 0) && bound == 2U) && _hj_key == & user->id) && *((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) && bound == 1U) && _hj_key == & user->id) && *((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_SFH_nondet_test3-1.i
        line: 745
        column: 4912
        function: main
      value: i <= 9998
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        column: 4912
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        column: 216
        function: main
      value: (((((2 <= i && 2 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _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) && _hj_key == & user->id) && *((int *)_hj_key)
        == 0) && (((((((((((bound <= 9999U && (((8U <= bound && _he_bkt_i == 64U)
        || (9U <= bound && _he_bkt_i == 128U)) || 7U <= bound)) || bound == 6U) ||
        (12U <= bound && bound <= 9999U)) || ((11U <= bound && bound <= 9999U) &&
        _he_bkt_i == 512U)) || ((7U <= bound && bound <= 9999U) && _he_bkt_i == 32U))
        || ((10U <= bound && bound <= 9999U) && _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_SFH_nondet_test3-1.i
        line: 750
        column: 551
        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_SFH_nondet_test3-1.i
        line: 750
        column: 551
        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_SFH_nondet_test3-1.i
        line: 750
        column: 551
        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_SFH_nondet_test3-1.i
        line: 750
        column: 551
        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_SFH_nondet_test3-1.i
        line: 750
        column: 551
        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_SFH_nondet_test3-1.i
        line: 750
        column: 551
        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_SFH_nondet_test3-1.i
        line: 750
        column: 551
        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_SFH_nondet_test3-1.i
        line: 750
        column: 551
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i == 256U))) || ((((0 ==
        i && i == 0) && bound == 2U) && _hj_key == & user->id) && *((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) && _hj_key == & user->id) && *((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_SFH_nondet_test3-1.i
        line: 745
        column: 227
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        column: 227
        function: main
      value: ((((((((((i <= 9998 && ((((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 <= 9998)) ||
        (((11 <= i && 12U <= bound) && i <= 9998) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9998) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9998) && _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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        column: 2685
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i == 256U))) || ((((0 ==
        i && i == 0) && bound == 2U) && _hj_key == & user->id) && *((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) && _hj_key == & user->id) && *((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_SFH_nondet_test3-1.i
        line: 745
        column: 39
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        column: 39
        function: main
      value: ((4UL == _hj_k && _hj_k == 4U) && ((((((((((i <= 9998 && ((((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 <= 9998)) || (((11 <= i && 12U <= bound) && i <=
        9998) && _he_bkt_i == 512U)) || (((7 <= i && 8U <= bound) && i <= 9998) &&
        _he_bkt_i == 32U)) || (((10 <= i && 11U <= bound) && i <= 9998) && _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_SFH_nondet_test3-1.i
        line: 750
        column: 13
        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_SFH_nondet_test3-1.i
        line: 750
        column: 13
        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_SFH_nondet_test3-1.i
        line: 750
        column: 13
        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_SFH_nondet_test3-1.i
        line: 750
        column: 13
        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_SFH_nondet_test3-1.i
        line: 750
        column: 13
        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_SFH_nondet_test3-1.i
        line: 750
        column: 13
        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_SFH_nondet_test3-1.i
        line: 750
        column: 13
        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_SFH_nondet_test3-1.i
        line: 750
        column: 13
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i == 256U))) || ((((0 ==
        i && i == 0) && bound == 2U) && _hj_key == & user->id) && *((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) && _hj_key == & user->id) && *((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_SFH_nondet_test3-1.i
        line: 745
        column: 4976
        function: main
      value: i <= 9998
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        column: 4976
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        column: 39
        function: main
      value: ((((4UL == _hj_k && _hj_k == _hj_k) && _hj_k == 4U) && (void *)_hj_key
        == (void *)(& i)) && (((((2 <= i && 2 <= *((int *)_hj_key)) && ((((((((i <=
        9998 && bound <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U
        <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) &&
        _he_bkt_i == 512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) &&
        *((int *)_hj_key) <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _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) && _hj_key == & user->id)
        && (((((((((((bound <= 9999U && (((8U <= bound && _he_bkt_i == 64U) || (9U
        <= bound && _he_bkt_i == 128U)) || 7U <= bound)) || bound == 6U) || (12U <=
        bound && bound <= 9999U)) || ((11U <= bound && bound <= 9999U) && _he_bkt_i
        == 512U)) || ((7U <= bound && bound <= 9999U) && _he_bkt_i == 32U)) || ((10U
        <= bound && bound <= 9999U) && _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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        column: 2856
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i == 256U))) || ((((0 ==
        i && i == 0) && bound == 2U) && _hj_key == & user->id) && *((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) && _hj_key == & user->id) && *((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_SFH_nondet_test3-1.i
        line: 745
        column: 4768
        function: main
      value: i <= 9998
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        column: 4768
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        column: 3062
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i == 256U))) || ((((0 ==
        i && i == 0) && bound == 2U) && _hj_key == & user->id) && *((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) && _hj_key == & user->id) && *((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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        column: 2612
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i == 256U))) || ((((0 ==
        i && i == 0) && bound == 2U) && _hj_key == & user->id) && *((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) && _hj_key == & user->id) && *((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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        column: 2670
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 750
        column: 762
        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_SFH_nondet_test3-1.i
        line: 750
        column: 762
        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_SFH_nondet_test3-1.i
        line: 750
        column: 762
        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_SFH_nondet_test3-1.i
        line: 750
        column: 762
        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_SFH_nondet_test3-1.i
        line: 750
        column: 762
        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_SFH_nondet_test3-1.i
        line: 750
        column: 762
        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_SFH_nondet_test3-1.i
        line: 750
        column: 762
        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_SFH_nondet_test3-1.i
        line: 750
        column: 762
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i == 256U))) || ((((0 ==
        i && i == 0) && bound == 2U) && _hj_key == & user->id) && *((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) && bound == 1U) && _hj_key == & user->id) && *((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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        column: 2513
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i == 256U))) || ((((0 ==
        i && i == 0) && bound == 2U) && _hj_key == & user->id) && *((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) && _hj_key == & user->id) && *((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_SFH_nondet_test3-1.i
        line: 747
        column: 5
        function: main
      value: ((((((4UL == _hj_k && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _hj_k == 4U) && (void *)_hj_key == (void *)(& i)) && (((((((((2 <= i &&
        2 <= *((int *)_hj_key)) && ((((((((i <= 10000 && bound <= 9999U) && *((int
        *)_hj_key) <= 10000) && (((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 <= 10000) && bound <= 9999U) &&
        *((int *)_hj_key) <= 10000)) || ((((11U <= bound && i <= 10000) && bound <=
        9999U) && *((int *)_hj_key) <= 10000) && _he_bkt_i == 512U)) || ((((7U <=
        bound && i <= 10000) && bound <= 9999U) && *((int *)_hj_key) <= 10000) &&
        _he_bkt_i == 32U)) || ((((10U <= bound && i <= 10000) && bound <= 9999U) &&
        *((int *)_hj_key) <= 10000) && _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 && bound == 1U) && *((int *)_hj_key) == 2))
        || ((((((0 == users && i == 2) && users == 0) && bound == 2U) && _hj_key ==
        & user->id) && _hj_key == & i) && *((int *)_hj_key) == 2)) || ((((((0 == users
        && i == 2) && users == 0) && bound == 1U) && _hj_key == & user->id) && _hj_key
        == & i) && *((int *)_hj_key) == 2))) || ((0 == i && i == 0) && ((((((((((((((((0
        == users && i == users) && users == 0) && bound == 0U) || (((((8U <= bound
        && bound <= 9999U) && 4UL == _hj_k) && _hj_k == 4U) && _hj_key == & user->id)
        && _he_bkt_i == 64U)) || (((((9U <= bound && bound <= 9999U) && 4UL == _hj_k)
        && _hj_k == 4U) && _hj_key == & user->id) && _he_bkt_i == 128U)) || ((((7U
        <= bound && bound <= 9999U) && 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 <= 9999U) && 4UL == _hj_k) &&
        _hj_k == 4U) && _hj_key == & user->id)) || (((((11U <= bound && bound <= 9999U)
        && 4UL == _hj_k) && _hj_k == 4U) && _hj_key == & user->id) && _he_bkt_i ==
        512U)) || (((((7U <= bound && bound <= 9999U) && 4UL == _hj_k) && _hj_k ==
        4U) && _hj_key == & user->id) && _he_bkt_i == 32U)) || (((((10U <= bound &&
        bound <= 9999U) && 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_SFH_nondet_test3-1.i
        line: 745
        column: 1832
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        column: 1832
        function: main
      value: ((((((((((i <= 9998 && ((((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 <= 9998)) ||
        (((11 <= i && 12U <= bound) && i <= 9998) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9998) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9998) && _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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        column: 1821
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i == 256U))) || ((((0 ==
        i && i == 0) && bound == 2U) && _hj_key == & user->id) && *((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) && _hj_key == & user->id) && *((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_SFH_nondet_test3-1.i
        line: 745
        column: 4104
        function: main
      value: i <= 9998
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        column: 4104
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 756
        column: 5
        function: main
      value: ((((((4UL == _hj_k && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _hj_k == 4U) && (void *)_hj_key == (void *)(& i)) && (((((((((((((i <=
        10000 && bound <= 9999U) && *((int *)_hj_key) <= 10000) && (((((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 <= 10000) && bound
        <= 9999U) && *((int *)_hj_key) <= 10000)) || ((((((11 <= i && 11 <= *((int
        *)_hj_key)) && 11U <= bound) && i <= 10000) && bound <= 9999U) && *((int *)_hj_key)
        <= 10000) && _he_bkt_i == 512U)) || ((((((7 <= i && 7 <= *((int *)_hj_key))
        && 7U <= bound) && i <= 10000) && bound <= 9999U) && *((int *)_hj_key) <=
        10000) && _he_bkt_i == 32U)) || ((((((10 <= i && 10 <= *((int *)_hj_key))
        && 10U <= bound) && i <= 10000) && bound <= 9999U) && *((int *)_hj_key) <=
        10000) && _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) && *((int *)_hj_key) == 2))) || (user == users && (((((((((((((((((((((((0
        == i && 0 == user) && 0 == users) && i == 0) && i == user) && i == users)
        && user == 0) && users == 0) && bound == 0U) || ((((((((((((8 <= i && 8 <=
        *((int *)_hj_key)) && 8U <= bound) && i <= 10000) && bound <= 9999U) && *((int
        *)_hj_key) <= 10000) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) &&
        _hj_k == _hj_k) && _he_bkt_i == 64U) && _hj_k == 4U) && (void *)_hj_key ==
        (void *)(& i))) || ((((((((((((9 <= i && 9 <= *((int *)_hj_key)) && 9U <=
        bound) && i <= 10000) && bound <= 9999U) && *((int *)_hj_key) <= 10000) &&
        4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i
        == 128U) && _hj_k == 4U) && (void *)_hj_key == (void *)(& i))) || (((((((((((7
        <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10000) && bound <=
        9999U) && *((int *)_hj_key) <= 10000) && 4UL == _hj_k) && 4UL == _hj_k) &&
        _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && (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) && (void *)_hj_key == (void *)(&
        i))) || (((((((((((12 <= i && 12 <= *((int *)_hj_key)) && 12U <= bound) &&
        i <= 10000) && bound <= 9999U) && *((int *)_hj_key) <= 10000) && 4UL == _hj_k)
        && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) && (void
        *)_hj_key == (void *)(& i))) || ((((((((((((11 <= i && 11 <= *((int *)_hj_key))
        && 11U <= bound) && i <= 10000) && bound <= 9999U) && *((int *)_hj_key) <=
        10000) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _he_bkt_i == 512U) && _hj_k == 4U) && (void *)_hj_key == (void *)(& i)))
        || ((((((((((((7 <= i && 7 <= *((int *)_hj_key)) && 7U <= bound) && i <= 10000)
        && bound <= 9999U) && *((int *)_hj_key) <= 10000) && 4UL == _hj_k) && 4UL
        == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k) && _he_bkt_i == 32U) && _hj_k
        == 4U) && (void *)_hj_key == (void *)(& i))) || ((((((((((((10 <= i && 10
        <= *((int *)_hj_key)) && 10U <= bound) && i <= 10000) && bound <= 9999U) &&
        *((int *)_hj_key) <= 10000) && 4UL == _hj_k) && 4UL == _hj_k) && _hj_k ==
        4U) && _hj_k == _hj_k) && _he_bkt_i == 256U) && _hj_k == 4U) && (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) && *((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) && (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) && (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) && (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) && *((int *)_hj_key) == 2) && (void *)_hj_key == (void *)(&
        i))) || (((((((((((((0 == user && 0 == users) && 4UL == _hj_k) && 4UL == _hj_k)
        && i == 2) && user == 0) && users == 0) && bound == 2U) && _hj_k == 4U) &&
        _hj_k == _hj_k) && _hj_k == 4U) && _hj_key == & i) && *((int *)_hj_key) ==
        2) && (void *)_hj_key == (void *)(& i))) || (((((((((((((0 == user && 0 ==
        users) && 4UL == _hj_k) && 4UL == _hj_k) && i == 2) && user == 0) && users
        == 0) && bound == 1U) && _hj_k == 4U) && _hj_k == _hj_k) && _hj_k == 4U) &&
        _hj_key == & i) && *((int *)_hj_key) == 2) && (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_SFH_nondet_test3-1.i
        line: 745
        column: 3578
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        column: 3578
        function: main
      value: ((((((((((i <= 9998 && ((((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 <= 9998)) ||
        (((11 <= i && 12U <= bound) && i <= 9998) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9998) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9998) && _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_SFH_nondet_test3-1.i
        line: 738
        column: 5
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 738
        column: 5
        function: main
      value: (((4UL == _hj_k && _hj_k == 4U) && _hj_key == & user->id) && (((((((((((i
        <= 9999 && ((((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 <= 9999)) || (((11 <=
        i && 11U <= bound) && i <= 9999) && _he_bkt_i == 512U)) || (((7 <= i && 7U
        <= bound) && i <= 9999) && _he_bkt_i == 32U)) || (((10 <= i && 10U <= bound)
        && i <= 9999) && _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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        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_SFH_nondet_test3-1.i
        line: 748
        column: 2456
        function: main
      value: ((((((0 <= i && 0 <= *((int *)_hj_key)) && ((((((((i <= 9998 && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && (((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 <= 9998)
        && bound <= 9999U) && *((int *)_hj_key) <= 9998)) || ((((11U <= bound && i
        <= 9998) && bound <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i ==
        512U)) || ((((7U <= bound && i <= 9998) && bound <= 9999U) && *((int *)_hj_key)
        <= 9998) && _he_bkt_i == 32U)) || ((((10U <= bound && i <= 9998) && bound
        <= 9999U) && *((int *)_hj_key) <= 9998) && _he_bkt_i == 256U))) || ((((0 ==
        i && i == 0) && bound == 2U) && _hj_key == & user->id) && *((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) && _hj_key == & user->id) && *((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_SFH_nondet_test3-1.i
        line: 745
        column: 3714
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        column: 3714
        function: main
      value: ((((((((((i <= 9998 && ((((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 <= 9998)) ||
        (((11 <= i && 12U <= bound) && i <= 9998) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9998) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9998) && _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_SFH_nondet_test3-1.i
        line: 745
        column: 3360
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        column: 3360
        function: main
      value: (((((((((i <= 9998 && ((((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 <= 9998)) ||
        (((11 <= i && 12U <= bound) && i <= 9998) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9998) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9998) && _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_SFH_nondet_test3-1.i
        line: 745
        column: 3631
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        column: 3631
        function: main
      value: ((((((((((i <= 9998 && ((((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 <= 9998)) ||
        (((11 <= i && 12U <= bound) && i <= 9998) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9998) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9998) && _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_SFH_nondet_test3-1.i
        line: 745
        column: 2467
        function: main
      value: bound <= 9999U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        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_SFH_nondet_test3-1.i
        line: 745
        column: 2467
        function: main
      value: ((((((((((i <= 9998 && ((((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 <= 9998)) ||
        (((11 <= i && 12U <= bound) && i <= 9998) && _he_bkt_i == 512U)) || (((7 <=
        i && 8U <= bound) && i <= 9998) && _he_bkt_i == 32U)) || (((10 <= i && 11U
        <= bound) && i <= 9998) && _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
