- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 10d5abeb-7e22-4f01-a271-b49c7bdb8f63
    creation_time: 2025-03-22T08:57:26Z
    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_test2-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i: 816e37c4bcf3aac0429d508c13e4e6eeab848e29c3869a32879e05a2b79a73a3
      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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 4912
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 4912
        function: main
      value: (i <= 9 && (((7 <= i && _he_bkt_i <= 63U) || (8 <= i && _he_bkt_i <=
        127U)) || (6 <= i && _he_bkt_i <= 31U))) || (_he_bkt_i <= 255U && i == 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 227
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 227
        function: main
      value: (((((((i <= 9 && (((8 <= i && _he_bkt_i == 64U) || (7 <= i && _he_bkt_i
        == 32U)) || 6 <= i)) || (i == 9 && _he_bkt_i == 128U)) || i == 5) || i ==
        4) || i == 2) || i == 3) || i == 1) || ((((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_test2-2.i
        line: 824
        column: 3062
        function: main
      value: 0 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 3062
        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_test2-2.i
        line: 824
        column: 3062
        function: main
      value: 0 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 3062
        function: main
      value: i <= 9
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 3062
        function: main
      value: '*((int *)_hj_key) <= 9'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        column: 2513
        function: main
      value: 0 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2513
        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_test2-2.i
        line: 824
        column: 2513
        function: main
      value: 0 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2513
        function: main
      value: i <= 9
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2513
        function: main
      value: '*((int *)_hj_key) <= 9'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        column: 216
        function: main
      value: ((((1 <= count_int_int && 2 <= i) && 2 <= *((int *)_hj_key)) && i <=
        9) && *((int *)_hj_key) <= 9) || (((0 == i && count_int_int == 0) && i ==
        0) && *((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_test2-2.i
        line: 833
        column: 848
        function: main
      value: 1 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 848
        function: main
      value: 10 <= i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 848
        function: main
      value: 10 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 848
        function: main
      value: i <= 11
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 848
        function: main
      value: '*((int *)_hj_key) <= 11'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 1832
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 1832
        function: main
      value: (((((((i <= 9 && (((8 <= i && _he_bkt_i == 64U) || (7 <= i && _he_bkt_i
        == 32U)) || 6 <= i)) || (i == 9 && _he_bkt_i == 128U)) || i == 5) || i ==
        4) || i == 2) || i == 3) || i == 1) || ((((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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 3360
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 3360
        function: main
      value: ((((((i <= 9 && (((8 <= i && _he_bkt_i == 64U) || (7 <= i && _he_bkt_i
        == 32U)) || 6 <= i)) || (i == 9 && _he_bkt_i == 128U)) || i == 5) || i ==
        4) || i == 2) || i == 3) || i == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 3631
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 3631
        function: main
      value: (((((((i <= 9 && (((8 <= i && _he_bkt_i == 64U) || (7 <= i && _he_bkt_i
        == 32U)) || 6 <= i)) || (i == 9 && _he_bkt_i == 128U)) || i == 5) || i ==
        4) || i == 2) || i == 3) || i == 1) || ((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_test2-2.i
        line: 821
        column: 39
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        column: 39
        function: main
      value: ((4UL == _hj_k && _hj_k == 4U) && (((((((i <= 9 && (((8 <= i && _he_bkt_i
        == 64U) || (7 <= i && _he_bkt_i == 32U)) || 6 <= i)) || (i == 9 && _he_bkt_i
        == 128U)) || i == 5) || i == 4) || i == 2) || i == 3) || i == 1)) || ((((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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 3714
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 3714
        function: main
      value: (((((((i <= 9 && (((8 <= i && _he_bkt_i == 64U) || (7 <= i && _he_bkt_i
        == 32U)) || 6 <= i)) || (i == 9 && _he_bkt_i == 128U)) || i == 5) || i ==
        4) || i == 2) || i == 3) || i == 1) || ((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_test2-2.i
        line: 814
        column: 5
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 814
        column: 5
        function: main
      value: (((4UL == _hj_k && _hj_k == 4U) && _hj_key == & user->id) && (((((((((i
        <= 10 && (((8 <= i && _he_bkt_i == 64U) || (7 <= i && _he_bkt_i == 32U)) ||
        7 <= i)) || (i == 10 && _he_bkt_i == 256U)) || ((9 <= i && i <= 10) && _he_bkt_i
        == 128U)) || i == 6) || i == 5) || i == 3) || i == 4) || i == 2) || (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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 4104
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 4104
        function: main
      value: (i <= 9 && (((8 <= i && _he_bkt_i == 64U) || (7 <= i && _he_bkt_i ==
        32U)) || 6 <= i)) || (i == 9 && _he_bkt_i == 128U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2685
        function: main
      value: 0 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2685
        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_test2-2.i
        line: 824
        column: 2685
        function: main
      value: 0 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2685
        function: main
      value: i <= 9
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2685
        function: main
      value: '*((int *)_hj_key) <= 9'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 833
        column: 7
        function: main
      value: 1 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 7
        function: main
      value: 10 <= i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 7
        function: main
      value: 10 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 7
        function: main
      value: i <= 11
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 7
        function: main
      value: '*((int *)_hj_key) <= 11'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 832
        column: 5
        function: main
      value: 1 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 832
        column: 5
        function: main
      value: 10 <= i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 832
        column: 5
        function: main
      value: 10 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 832
        column: 5
        function: main
      value: i <= 11
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 832
        column: 5
        function: main
      value: '*((int *)_hj_key) <= 11'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 832
        column: 5
        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_test2-2.i
        line: 832
        column: 5
        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_test2-2.i
        line: 832
        column: 5
        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_test2-2.i
        line: 832
        column: 5
        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_test2-2.i
        line: 832
        column: 5
        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_test2-2.i
        line: 832
        column: 5
        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_test2-2.i
        line: 824
        column: 1821
        function: main
      value: 0 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 1821
        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_test2-2.i
        line: 824
        column: 1821
        function: main
      value: 0 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 1821
        function: main
      value: i <= 9
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 1821
        function: main
      value: '*((int *)_hj_key) <= 9'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 2467
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 2467
        function: main
      value: (((((((i <= 9 && (((8 <= i && _he_bkt_i == 64U) || (7 <= i && _he_bkt_i
        == 32U)) || 6 <= i)) || (i == 9 && _he_bkt_i == 128U)) || i == 5) || i ==
        4) || i == 2) || i == 3) || i == 1) || ((((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_test2-2.i
        line: 833
        column: 546
        function: main
      value: 1 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 546
        function: main
      value: 10 <= i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 546
        function: main
      value: 10 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 546
        function: main
      value: i <= 11
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 546
        function: main
      value: '*((int *)_hj_key) <= 11'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        column: 757
        function: main
      value: 1 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 757
        function: main
      value: 10 <= i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 757
        function: main
      value: 10 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 757
        function: main
      value: i <= 11
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        column: 757
        function: main
      value: '*((int *)_hj_key) <= 11'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 833
        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_test2-2.i
        line: 824
        column: 2612
        function: main
      value: 0 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2612
        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_test2-2.i
        line: 824
        column: 2612
        function: main
      value: 0 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2612
        function: main
      value: i <= 9
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2612
        function: main
      value: '*((int *)_hj_key) <= 9'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 4976
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 4976
        function: main
      value: (i <= 9 && (((7 <= i && _he_bkt_i <= 63U) || (8 <= i && _he_bkt_i <=
        127U)) || (6 <= i && _he_bkt_i <= 31U))) || (_he_bkt_i <= 255U && i == 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 4768
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 4768
        function: main
      value: (i <= 9 && (((7 <= i && _he_bkt_i <= 64U) || (8 <= i && _he_bkt_i <=
        128U)) || (6 <= i && _he_bkt_i <= 32U))) || (_he_bkt_i <= 256U && i == 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 3578
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 3578
        function: main
      value: (((((((i <= 9 && (((8 <= i && _he_bkt_i == 64U) || (7 <= i && _he_bkt_i
        == 32U)) || 6 <= i)) || (i == 9 && _he_bkt_i == 128U)) || i == 5) || i ==
        4) || i == 2) || i == 3) || i == 1) || ((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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        column: 39
        function: main
      value: (((((((((1 <= count_int_int && 2 <= i) && 2 <= *((int *)_hj_key)) &&
        i <= 9) && *((int *)_hj_key) <= 9) && 4UL == _hj_k) && _hj_k == _hj_k) &&
        _hj_k == 4U) && _hj_key == & i) && (void *)_hj_key == (void *)(& i)) || ((0
        == i && count_int_int == 0) && 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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        column: 2670
        function: main
      value: count_int_int == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 821
        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_test2-2.i
        line: 824
        column: 2456
        function: main
      value: 0 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2456
        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_test2-2.i
        line: 824
        column: 2456
        function: main
      value: 0 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2456
        function: main
      value: i <= 9
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2456
        function: main
      value: '*((int *)_hj_key) <= 9'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        column: 2856
        function: main
      value: 0 <= count_int_int
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2856
        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_test2-2.i
        line: 824
        column: 2856
        function: main
      value: 0 <= *((int *)_hj_key)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2856
        function: main
      value: i <= 9
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        column: 2856
        function: main
      value: '*((int *)_hj_key) <= 9'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_JEN_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 824
        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_test2-2.i
        line: 823
        column: 5
        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_test2-2.i
        line: 823
        column: 5
        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_test2-2.i
        line: 823
        column: 5
        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_test2-2.i
        line: 823
        column: 5
        function: main
      value: (((((((((1 <= count_int_int && 2 <= i) && 2 <= *((int *)_hj_key)) &&
        i <= 11) && *((int *)_hj_key) <= 11) && 4UL == _hj_k) && _hj_k == _hj_k) &&
        _hj_k == 4U) && _hj_key == & i) && (void *)_hj_key == (void *)(& i)) || ((0
        == i && count_int_int == 0) && i == 0)
      format: c_expression
