- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: b2a44469-c550-469d-bc92-ab80dff61caf
    creation_time: 2025-03-22T09:06:17Z
    producer:
      name: Goblint
      version: heads/master-0-g66dff5a90-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp.json'' ''--disable'' ''witness.graphml.enabled''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i: 112ef0f8366461020cac5f2ac7dec2d7e41f31b24e653cd7734885d2bb23b087
      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_OAT_nondet_test1-2.i
        line: 737
        column: 5
        function: main
      value: (((4UL == _hj_k && _hj_k == 4U) && _hj_key == & user->id) && (((((((((i
        <= 10 && (((8 <= i && _he_bkt_i == 64U) || (9 <= i && _he_bkt_i == 128U))
        || (7 <= i && _he_bkt_i == 32U))) || ((-163840 <= sum && sum <= 163835) &&
        i == 5)) || (7 <= i && i <= 10)) || ((-196608 <= sum && sum <= 196602) &&
        i == 6)) || (i == 10 && _he_bkt_i == 256U)) || ((-131072 <= sum && sum <=
        131068) && i == 4)) || ((-98304 <= sum && sum <= 98301) && i == 3)) || ((-65536
        <= sum && sum <= 65534) && i == 2)) || (((-32768 <= sum && sum <= 32767) &&
        i == 1) && user == users))) || ((((((((0 == i && 0 == users) && 0 == sum)
        && i == 0) && i == users) && i == sum) && users == 0) && users == sum) &&
        sum == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 745
        column: 39
        function: main
      value: ((4UL == _hj_k && _hj_k == 4U) && ((((((((((8 <= i && i <= 9) && _he_bkt_i
        == 64U) || (i == 9 && _he_bkt_i == 128U)) || ((7 <= i && i <= 9) && _he_bkt_i
        == 32U)) || ((-163840 <= sum && sum <= 163835) && i == 4)) || (6 <= i && i
        <= 9)) || ((-196608 <= sum && sum <= 196602) && i == 5)) || ((-131072 <= sum
        && sum <= 131068) && i == 3)) || ((-98304 <= sum && sum <= 98301) && i ==
        2)) || ((-65536 <= sum && sum <= 65534) && i == 1))) || ((((((-32768 <= sum
        && sum <= 32767) && 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_OAT_nondet_test1-2.i
        line: 747
        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_OAT_nondet_test1-2.i
        line: 747
        column: 5
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 747
        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_OAT_nondet_test1-2.i
        line: 745
        column: 2670
        function: main
      value: -32768 <= sum
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 745
        column: 2670
        function: main
      value: sum <= 32767
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.i
        line: 745
        column: 4976
        function: main
      value: ((i <= 9 && ((8 <= i && _he_bkt_i <= 127U) || (7 <= i && _he_bkt_i <=
        63U))) || (_he_bkt_i <= 255U && i == 9)) || ((6 <= i && i <= 9) && _he_bkt_i
        <= 31U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 753
        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_OAT_nondet_test1-2.i
        line: 753
        column: 757
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 753
        column: 757
        function: main
      value: sum == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 753
        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_OAT_nondet_test1-2.i
        line: 753
        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_OAT_nondet_test1-2.i
        line: 753
        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_OAT_nondet_test1-2.i
        line: 753
        column: 7
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 753
        column: 7
        function: main
      value: sum == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 753
        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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.i
        line: 745
        column: 3714
        function: main
      value: ((((((((((8 <= i && i <= 9) && _he_bkt_i == 64U) || (i == 9 && _he_bkt_i
        == 128U)) || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || ((-163840 <= sum
        && sum <= 163835) && i == 4)) || (6 <= i && i <= 9)) || ((-196608 <= sum &&
        sum <= 196602) && i == 5)) || ((-131072 <= sum && sum <= 131068) && i == 3))
        || ((-98304 <= sum && sum <= 98301) && i == 2)) || ((-65536 <= sum && sum
        <= 65534) && i == 1)) || ((((-32768 <= sum && sum <= 32767) && 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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.i
        line: 745
        column: 4104
        function: main
      value: ((((8 <= i && i <= 9) && _he_bkt_i == 64U) || (i == 9 && _he_bkt_i ==
        128U)) || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || (6 <= i && i <= 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 753
        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_OAT_nondet_test1-2.i
        line: 753
        column: 546
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 753
        column: 546
        function: main
      value: sum == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 753
        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_OAT_nondet_test1-2.i
        line: 753
        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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.i
        line: 745
        column: 2467
        function: main
      value: ((((((((((((((-32768 <= sum && sum <= 32767) && 0 == i) && 0 == users)
        && i == 0) && i == users) && users == 0) || ((8 <= i && i <= 9) && _he_bkt_i
        == 64U)) || (i == 9 && _he_bkt_i == 128U)) || ((7 <= i && i <= 9) && _he_bkt_i
        == 32U)) || ((-163840 <= sum && sum <= 163835) && i == 4)) || (6 <= i && i
        <= 9)) || ((-196608 <= sum && sum <= 196602) && i == 5)) || ((-131072 <= sum
        && sum <= 131068) && i == 3)) || ((-98304 <= sum && sum <= 98301) && i ==
        2)) || ((-65536 <= sum && sum <= 65534) && i == 1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.i
        line: 745
        column: 227
        function: main
      value: ((((((((((8 <= i && i <= 9) && _he_bkt_i == 64U) || (i == 9 && _he_bkt_i
        == 128U)) || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || ((-163840 <= sum
        && sum <= 163835) && i == 4)) || (6 <= i && i <= 9)) || ((-196608 <= sum &&
        sum <= 196602) && i == 5)) || ((-131072 <= sum && sum <= 131068) && i == 3))
        || ((-98304 <= sum && sum <= 98301) && i == 2)) || ((-65536 <= sum && sum
        <= 65534) && i == 1)) || ((((((-32768 <= sum && sum <= 32767) && 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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.i
        line: 745
        column: 3578
        function: main
      value: ((((((((((8 <= i && i <= 9) && _he_bkt_i == 64U) || (i == 9 && _he_bkt_i
        == 128U)) || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || ((-163840 <= sum
        && sum <= 163835) && i == 4)) || (6 <= i && i <= 9)) || ((-196608 <= sum &&
        sum <= 196602) && i == 5)) || ((-131072 <= sum && sum <= 131068) && i == 3))
        || ((-98304 <= sum && sum <= 98301) && i == 2)) || ((-65536 <= sum && sum
        <= 65534) && i == 1)) || ((((-32768 <= sum && sum <= 32767) && 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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.i
        line: 745
        column: 4768
        function: main
      value: ((i <= 9 && ((8 <= i && _he_bkt_i <= 128U) || (7 <= i && _he_bkt_i <=
        64U))) || (_he_bkt_i <= 256U && i == 9)) || ((6 <= i && i <= 9) && _he_bkt_i
        <= 32U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.i
        line: 745
        column: 1832
        function: main
      value: ((((((((((((((-32768 <= sum && sum <= 32767) && 0 == i) && 0 == users)
        && i == 0) && i == users) && users == 0) || ((8 <= i && i <= 9) && _he_bkt_i
        == 64U)) || (i == 9 && _he_bkt_i == 128U)) || ((7 <= i && i <= 9) && _he_bkt_i
        == 32U)) || ((-163840 <= sum && sum <= 163835) && i == 4)) || (6 <= i && i
        <= 9)) || ((-196608 <= sum && sum <= 196602) && i == 5)) || ((-131072 <= sum
        && sum <= 131068) && i == 3)) || ((-98304 <= sum && sum <= 98301) && i ==
        2)) || ((-65536 <= sum && sum <= 65534) && i == 1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 753
        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_OAT_nondet_test1-2.i
        line: 753
        column: 848
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 753
        column: 848
        function: main
      value: sum == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 753
        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_OAT_nondet_test1-2.i
        line: 753
        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_OAT_nondet_test1-2.i
        line: 752
        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_OAT_nondet_test1-2.i
        line: 752
        column: 5
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 752
        column: 5
        function: main
      value: sum == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.i
        line: 752
        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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.i
        line: 745
        column: 3360
        function: main
      value: (((((((((8 <= i && i <= 9) && _he_bkt_i == 64U) || (i == 9 && _he_bkt_i
        == 128U)) || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || ((-163840 <= sum
        && sum <= 163835) && i == 4)) || (6 <= i && i <= 9)) || ((-196608 <= sum &&
        sum <= 196602) && i == 5)) || ((-131072 <= sum && sum <= 131068) && i == 3))
        || ((-98304 <= sum && sum <= 98301) && i == 2)) || ((-65536 <= sum && sum
        <= 65534) && i == 1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.i
        line: 745
        column: 4912
        function: main
      value: ((i <= 9 && ((8 <= i && _he_bkt_i <= 127U) || (7 <= i && _he_bkt_i <=
        63U))) || (_he_bkt_i <= 255U && i == 9)) || ((6 <= i && i <= 9) && _he_bkt_i
        <= 31U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.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_OAT_nondet_test1-2.i
        line: 745
        column: 3631
        function: main
      value: ((((((((((8 <= i && i <= 9) && _he_bkt_i == 64U) || (i == 9 && _he_bkt_i
        == 128U)) || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || ((-163840 <= sum
        && sum <= 163835) && i == 4)) || (6 <= i && i <= 9)) || ((-196608 <= sum &&
        sum <= 196602) && i == 5)) || ((-131072 <= sum && sum <= 131068) && i == 3))
        || ((-98304 <= sum && sum <= 98301) && i == 2)) || ((-65536 <= sum && sum
        <= 65534) && i == 1)) || ((((-32768 <= sum && sum <= 32767) && 0 == i) &&
        i == 0) && user == users)
      format: c_expression
