- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 0ebe25a1-92c9-4a14-811f-fcab2fd02404
    creation_time: 2025-03-22T08:39: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_FNV_test5-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i: c7b5cea41c34641368705a00e3051c009f6877551b3530b7d4fceaf386f5f58c
      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_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: 0 == i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: 0 == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        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_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: i == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: i == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: user == users
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: altusers == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2691
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: 0x9e3779b9u == _hj_i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: 0x9e3779b9u == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: 0xfeedbeefu == _ha_hashv
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        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_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: _ha_hashv == 4276993775U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: _hj_i == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: _hj_i == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: _hj_j == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 231
        function: main
      value: (users == altusers && (((((((((((((((((((((_he_bkt_i == 64U && ((((8
        <= i && i <= 9) && ((_he_bkt_i == 64U || _he_bkt_i == 32U) || _he_bkt_i ==
        128U)) || (i == 9 && _he_bkt_i == 256U)) || (8 <= i && i <= 9))) || ((i ==
        9 && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i
        == 64U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i == 64U))
        || ((i == 9 && _he_bkt_i == 32U) && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i
        == 128U) && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (i == 9 && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i
        == 32U) && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i == 128U)
        && _he_bkt_i == 32U)) || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i == 32U))
        || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _he_bkt_i
        == 32U)) || ((8 <= i && i <= 9) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 256U)) || (6 <= i && i <= 9)) || i == 5) || i == 4) || i == 3) || i ==
        2) || i == 1)) || (((((0 == i && 0 == altusers) && i == 0) && i == altusers)
        && user == users) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 1836
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 1836
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 1836
        function: main
      value: 0x9e3779b9u == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 1836
        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_FNV_test5-1.i
        line: 744
        column: 1836
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 1836
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 1836
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 1836
        function: main
      value: _ha_hashv == 4276993779U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 1836
        function: main
      value: _hj_j == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 1836
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 1836
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 1836
        function: main
      value: (users == altusers && (((((((((((((((((((((_he_bkt_i == 64U && ((((8
        <= i && i <= 9) && ((_he_bkt_i == 64U || _he_bkt_i == 32U) || _he_bkt_i ==
        128U)) || (i == 9 && _he_bkt_i == 256U)) || (8 <= i && i <= 9))) || ((i ==
        9 && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i
        == 64U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i == 64U))
        || ((i == 9 && _he_bkt_i == 32U) && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i
        == 128U) && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (i == 9 && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i
        == 32U) && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i == 128U)
        && _he_bkt_i == 32U)) || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i == 32U))
        || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _he_bkt_i
        == 32U)) || ((8 <= i && i <= 9) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 256U)) || (6 <= i && i <= 9)) || i == 5) || i == 4) || i == 3) || i ==
        2) || i == 1)) || (((((0 == i && 0 == altusers) && i == 0) && i == altusers)
        && user == users) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4976
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4976
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4976
        function: main
      value: ((((((((((((_he_bkt_i == 64U && (((8 <= i && i <= 9) && ((_he_bkt_i <=
        63U || _he_bkt_i <= 127U) || _he_bkt_i <= 31U)) || (_he_bkt_i <= 255U && i
        == 9))) || ((_he_bkt_i <= 63U && i == 9) && _he_bkt_i == 128U)) || ((_he_bkt_i
        <= 127U && i == 9) && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i
        <= 63U) && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i <= 127U)
        && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i <= 63U)) || ((8
        <= i && i <= 9) && _he_bkt_i <= 127U)) || ((_he_bkt_i <= 31U && i == 9) &&
        _he_bkt_i == 128U)) || ((_he_bkt_i <= 255U && i == 9) && _he_bkt_i == 128U))
        || (((7 <= i && i <= 9) && _he_bkt_i <= 31U) && _he_bkt_i == 32U)) || ((_he_bkt_i
        <= 255U && i == 9) && _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _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_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        function: main
      value: 0 <= j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        function: main
      value: j <= 81
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2879
        function: main
      value: '*((int *)_hj_key) <= 81'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2879
        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_FNV_test5-1.i
        line: 748
        column: 2879
        function: main
      value: _hj_key == & j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2879
        function: main
      value: (void *)_hj_key == (void *)(& j)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 2467
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 2467
        function: main
      value: (((((4UL == _hj_k && _hj_k == _hj_k) && _hj_k == 4U) && ((((((((((((((((_he_bkt_i
        == 64U && ((((8 <= i && i <= 9) && (_he_bkt_i == 64U || _he_bkt_i == 32U))
        || (i == 9 && _he_bkt_i == 128U)) || (8 <= i && i <= 9))) || ((i == 9 && _he_bkt_i
        == 64U) && _he_bkt_i == 128U)) || (((8 <= i && i <= 9) && _he_bkt_i == 64U)
        && _he_bkt_i == 32U)) || ((8 <= i && i <= 9) && _he_bkt_i == 64U)) || ((i
        == 9 && _he_bkt_i == 32U) && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i
        == 128U) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i == 128U)) || (((7
        <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i == 32U)) || ((i == 9 &&
        _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i
        == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || (i == 9 && _he_bkt_i
        == 128U)) || (6 <= i && i <= 9)) || i == 5) || i == 4) || i == 3)) || (((((((0
        == i && 0 == users) && 0 == altusers) && i == 0) && i == users) && i == altusers)
        && users == 0) && altusers == 0)) || (((4UL == _hj_k && i == 2) && _hj_k ==
        _hj_k) && _hj_k == 4U)) || (((4UL == _hj_k && i == 1) && _hj_k == _hj_k) &&
        _hj_k == 4U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 1832
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 1832
        function: main
      value: (((((4UL == _hj_k && _hj_k == _hj_k) && _hj_k == 4U) && ((((((((((((((((_he_bkt_i
        == 64U && ((((8 <= i && i <= 9) && (_he_bkt_i == 64U || _he_bkt_i == 32U))
        || (i == 9 && _he_bkt_i == 128U)) || (8 <= i && i <= 9))) || ((i == 9 && _he_bkt_i
        == 64U) && _he_bkt_i == 128U)) || (((8 <= i && i <= 9) && _he_bkt_i == 64U)
        && _he_bkt_i == 32U)) || ((8 <= i && i <= 9) && _he_bkt_i == 64U)) || ((i
        == 9 && _he_bkt_i == 32U) && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i
        == 128U) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i == 128U)) || (((7
        <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i == 32U)) || ((i == 9 &&
        _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i
        == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || (i == 9 && _he_bkt_i
        == 128U)) || (6 <= i && i <= 9)) || i == 5) || i == 4) || i == 3)) || (((((((0
        == i && 0 == users) && 0 == altusers) && i == 0) && i == users) && i == altusers)
        && users == 0) && altusers == 0)) || (((4UL == _hj_k && i == 2) && _hj_k ==
        _hj_k) && _hj_k == 4U)) || (((4UL == _hj_k && i == 1) && _hj_k == _hj_k) &&
        _hj_k == 4U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 2670
        function: main
      value: 0 == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 2670
        function: main
      value: i == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 2670
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        column: 2670
        function: main
      value: altusers == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 39
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        column: 39
        function: main
      value: (((((4UL == _hj_k && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _hj_k == 4U) && ((((((((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <=
        9) && (_he_bkt_i == 64U || _he_bkt_i == 32U)) || (i == 9 && _he_bkt_i == 128U))
        || (8 <= i && i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i == 128U))
        || (((8 <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || ((8
        <= i && i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U) &&
        _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U))
        || (i == 9 && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i ==
        32U) && _he_bkt_i == 32U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i
        == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || ((7 <= i && i <=
        9) && _he_bkt_i == 32U)) || (i == 9 && _he_bkt_i == 128U)) || (6 <= i && i
        <= 9)) || i == 5) || i == 4) || i == 3) || i == 2) || i == 1)) || (((((((0
        == i && 0 == users) && 0 == altusers) && i == 0) && i == users) && i == altusers)
        && users == 0) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        function: main
      value: 0 <= j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        function: main
      value: j <= 81
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2698
        function: main
      value: '*((int *)_hj_key) <= 81'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2698
        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_FNV_test5-1.i
        line: 748
        column: 2698
        function: main
      value: _hj_key == & j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2698
        function: main
      value: (void *)_hj_key == (void *)(& j)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        function: main
      value: 0 <= j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        function: main
      value: j <= 81
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2620
        function: main
      value: '*((int *)_hj_key) <= 81'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2620
        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_FNV_test5-1.i
        line: 748
        column: 2620
        function: main
      value: _hj_key == & j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2620
        function: main
      value: (void *)_hj_key == (void *)(& j)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 746
        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_FNV_test5-1.i
        line: 746
        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_FNV_test5-1.i
        line: 746
        column: 5
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 746
        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_FNV_test5-1.i
        line: 746
        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_FNV_test5-1.i
        line: 746
        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_FNV_test5-1.i
        line: 746
        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_FNV_test5-1.i
        line: 746
        column: 5
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 746
        column: 5
        function: main
      value: ((0 == i && count_int_int == 0) && i == 0) || ((((((((((((0 <= j && 0
        <= *((int *)_hj_key)) && 1 <= count_int_int) && 2 <= i) && i <= 11) && j <=
        81) && *((int *)_hj_key) <= 81) && 4UL == _hj_k) && _hj_k == _hj_k) && _hj_k
        == _hj_k) && _hj_k == 4U) && _hj_key == & j) && (void *)_hj_key == (void *)(&
        j))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5106
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5106
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5106
        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_FNV_test5-1.i
        line: 744
        column: 5106
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5106
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5106
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5106
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5106
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5106
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5106
        function: main
      value: ((((((((((((((((i <= 9 && (((_he_bkt_i == 64U && ((8 <= i && _he_bkt_i
        <= 127U) || (7 <= i && _he_bkt_i <= 63U))) || ((8 <= i && _he_bkt_i <= 127U)
        && _he_bkt_i == 32U)) || ((8 <= i && _he_bkt_i <= 127U) && _he_bkt_i == 128U)))
        || ((_he_bkt_i <= 127U && i == 9) && _he_bkt_i == 256U)) || ((8 <= i && i
        <= 9) && _he_bkt_i <= 127U)) || (((7 <= i && i <= 9) && _he_bkt_i <= 63U)
        && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i <= 63U) && _he_bkt_i
        == 128U)) || ((_he_bkt_i <= 63U && i == 9) && _he_bkt_i == 256U)) || ((7 <=
        i && i <= 9) && _he_bkt_i <= 63U)) || ((_he_bkt_i <= 255U && i == 9) && _he_bkt_i
        == 64U)) || (((7 <= i && i <= 9) && _he_bkt_i <= 31U) && _he_bkt_i == 64U))
        || ((_he_bkt_i <= 255U && i == 9) && _he_bkt_i == 32U)) || ((_he_bkt_i <=
        255U && i == 9) && _he_bkt_i == 128U)) || ((_he_bkt_i <= 255U && i == 9) &&
        _he_bkt_i == 256U)) || (_he_bkt_i <= 255U && i == 9)) || (((6 <= i && i <=
        9) && _he_bkt_i <= 31U) && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i
        <= 31U) && _he_bkt_i == 128U)) || ((_he_bkt_i <= 31U && i == 9) && _he_bkt_i
        == 256U)) || ((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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 3360
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 3360
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 3360
        function: main
      value: (((((((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <= 9) && (_he_bkt_i
        == 64U || _he_bkt_i == 32U)) || (i == 9 && _he_bkt_i == 128U)) || (8 <= i
        && i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((8
        <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || ((8 <= i &&
        i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U) && _he_bkt_i
        == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (i ==
        9 && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i
        == 32U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((7 <=
        i && i <= 9) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i ==
        32U)) || (i == 9 && _he_bkt_i == 128U)) || (6 <= i && i <= 9)) || i == 5)
        || i == 4) || i == 3) || i == 2) || i == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4768
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4768
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4768
        function: main
      value: ((((((((((((_he_bkt_i == 64U && (((8 <= i && i <= 9) && ((_he_bkt_i <=
        64U || _he_bkt_i <= 128U) || _he_bkt_i <= 32U)) || (_he_bkt_i <= 256U && i
        == 9))) || ((_he_bkt_i <= 64U && i == 9) && _he_bkt_i == 128U)) || ((_he_bkt_i
        <= 128U && i == 9) && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i
        <= 64U) && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i <= 128U)
        && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i <= 64U)) || ((8
        <= i && i <= 9) && _he_bkt_i <= 128U)) || ((_he_bkt_i <= 32U && i == 9) &&
        _he_bkt_i == 128U)) || ((_he_bkt_i <= 256U && i == 9) && _he_bkt_i == 128U))
        || (((7 <= i && i <= 9) && _he_bkt_i <= 32U) && _he_bkt_i == 32U)) || ((_he_bkt_i
        <= 256U && i == 9) && _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _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_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: 0 <= j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: j <= 81
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: '*((int *)_hj_key) <= 81'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: _hj_key == & j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2456
        function: main
      value: (void *)_hj_key == (void *)(& j)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3419
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3419
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3419
        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_FNV_test5-1.i
        line: 744
        column: 3419
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3419
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3419
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3419
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3419
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3419
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3419
        function: main
      value: ((((((((((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <= 9) && ((_he_bkt_i
        == 64U || _he_bkt_i == 32U) || _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 256U)) || (8 <= i && i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U))
        || ((7 <= i && i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U))
        || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i == 32U))
        || (((8 <= i && i <= 9) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((i
        == 9 && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) &&
        _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _he_bkt_i == 32U)) || ((8 <=
        i && i <= 9) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i == 256U)) || (6
        <= i && i <= 9)) || i == 5) || i == 4) || i == 3) || i == 2) || i == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4104
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4104
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4104
        function: main
      value: ((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <= 9) && (_he_bkt_i ==
        64U || _he_bkt_i == 32U)) || (i == 9 && _he_bkt_i == 128U)) || (8 <= i &&
        i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((8
        <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || ((8 <= i &&
        i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U) && _he_bkt_i
        == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (i ==
        9 && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i
        == 32U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((7 <=
        i && i <= 9) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i ==
        32U)) || (i == 9 && _he_bkt_i == 128U)) || (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_FNV_test5-1.i
        line: 736
        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_FNV_test5-1.i
        line: 736
        column: 5
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 736
        column: 5
        function: main
      value: (((((((4UL == _hj_k && 4UL == _hj_k) && _hj_k == 4U) && _hj_k == _hj_k)
        && _hj_key == & user->id) && _hj_k == 4U) && _hj_key == & user->cookie) &&
        (((((((((((((((((((((((((((_he_bkt_i == 64U && (((i <= 10 && ((8 <= i && (_he_bkt_i
        == 64U || _he_bkt_i == 32U)) || (9 <= i && _he_bkt_i == 128U))) || (i == 10
        && _he_bkt_i == 256U)) || (8 <= i && i <= 10))) || (((9 <= i && i <= 10) &&
        _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((8 <= i && i <= 10) && _he_bkt_i
        == 64U) && _he_bkt_i == 32U)) || ((8 <= i && i <= 10) && _he_bkt_i == 64U))
        || ((i == 10 && _he_bkt_i == 64U) && _he_bkt_i == 256U)) || (((9 <= i && i
        <= 10) && _he_bkt_i == 32U) && _he_bkt_i == 128U)) || (((9 <= i && i <= 10)
        && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || ((i == 10 && _he_bkt_i ==
        256U) && _he_bkt_i == 128U)) || ((9 <= i && i <= 10) && _he_bkt_i == 128U))
        || (((7 <= i && i <= 10) && _he_bkt_i == 32U) && _he_bkt_i == 32U)) || (((9
        <= i && i <= 10) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((i == 10
        && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 10) && _he_bkt_i
        == 32U)) || ((7 <= i && i <= 10) && _he_bkt_i == 32U)) || ((i == 10 && _he_bkt_i
        == 32U) && _he_bkt_i == 256U)) || ((9 <= i && i <= 10) && _he_bkt_i == 128U))
        || (i == 10 && _he_bkt_i == 256U)) || (7 <= i && i <= 10)) || ((i == 10 &&
        _he_bkt_i == 128U) && _he_bkt_i == 256U)) || ((i == 10 && _he_bkt_i == 256U)
        && _he_bkt_i == 256U)) || (i == 10 && _he_bkt_i == 256U)) || i == 6) || i
        == 5) || i == 4) || i == 3) || i == 2) || ((i == 1 && user == users) && user
        == altusers))) || (((((((0 == i && 0 == users) && 0 == altusers) && i == 0)
        && i == users) && i == altusers) && users == 0) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4894
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4894
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4894
        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_FNV_test5-1.i
        line: 744
        column: 4894
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4894
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4894
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4894
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4894
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4894
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4894
        function: main
      value: ((((((((((((((((i <= 9 && (((_he_bkt_i == 64U && ((8 <= i && _he_bkt_i
        <= 128U) || (7 <= i && _he_bkt_i <= 64U))) || ((8 <= i && _he_bkt_i <= 128U)
        && _he_bkt_i == 32U)) || ((8 <= i && _he_bkt_i <= 128U) && _he_bkt_i == 128U)))
        || ((_he_bkt_i <= 128U && i == 9) && _he_bkt_i == 256U)) || ((8 <= i && i
        <= 9) && _he_bkt_i <= 128U)) || (((7 <= i && i <= 9) && _he_bkt_i <= 64U)
        && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i <= 64U) && _he_bkt_i
        == 128U)) || ((_he_bkt_i <= 64U && i == 9) && _he_bkt_i == 256U)) || ((7 <=
        i && i <= 9) && _he_bkt_i <= 64U)) || ((_he_bkt_i <= 256U && i == 9) && _he_bkt_i
        == 64U)) || (((7 <= i && i <= 9) && _he_bkt_i <= 32U) && _he_bkt_i == 64U))
        || ((_he_bkt_i <= 256U && i == 9) && _he_bkt_i == 32U)) || ((_he_bkt_i <=
        256U && i == 9) && _he_bkt_i == 128U)) || ((_he_bkt_i <= 256U && i == 9) &&
        _he_bkt_i == 256U)) || (_he_bkt_i <= 256U && i == 9)) || (((6 <= i && i <=
        9) && _he_bkt_i <= 32U) && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i
        <= 32U) && _he_bkt_i == 128U)) || ((_he_bkt_i <= 32U && i == 9) && _he_bkt_i
        == 256U)) || ((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_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        function: main
      value: 0 <= j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        function: main
      value: j <= 81
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 3093
        function: main
      value: '*((int *)_hj_key) <= 81'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 3093
        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_FNV_test5-1.i
        line: 748
        column: 3093
        function: main
      value: _hj_key == & j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 3093
        function: main
      value: (void *)_hj_key == (void *)(& j)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: 0 <= j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: j <= 81
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: '*((int *)_hj_key) <= 81'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: 0x9e3779b9u == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: _hf_hashv == 4276993779U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: _hj_j == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: _hj_key == & j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 1821
        function: main
      value: (void *)_hj_key == (void *)(& j)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 3714
        function: main
      value: ((((4UL == _hj_k && users == altusers) && _hj_k == _hj_k) && _hj_k ==
        4U) && ((((((((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <= 9) && (_he_bkt_i
        == 64U || _he_bkt_i == 32U)) || (i == 9 && _he_bkt_i == 128U)) || (8 <= i
        && i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((8
        <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || ((8 <= i &&
        i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U) && _he_bkt_i
        == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (i ==
        9 && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i
        == 32U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((7 <=
        i && i <= 9) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i ==
        32U)) || (i == 9 && _he_bkt_i == 128U)) || (6 <= i && i <= 9)) || i == 5)
        || i == 4) || i == 3) || i == 2) || i == 1)) || (((((0 == i && 0 == altusers)
        && i == 0) && i == altusers) && user == users) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 227
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 227
        function: main
      value: (((4UL == _hj_k && _hj_k == _hj_k) && _hj_k == 4U) && ((((((((((((((((((_he_bkt_i
        == 64U && ((((8 <= i && i <= 9) && (_he_bkt_i == 64U || _he_bkt_i == 32U))
        || (i == 9 && _he_bkt_i == 128U)) || (8 <= i && i <= 9))) || ((i == 9 && _he_bkt_i
        == 64U) && _he_bkt_i == 128U)) || (((8 <= i && i <= 9) && _he_bkt_i == 64U)
        && _he_bkt_i == 32U)) || ((8 <= i && i <= 9) && _he_bkt_i == 64U)) || ((i
        == 9 && _he_bkt_i == 32U) && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i
        == 128U) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i == 128U)) || (((7
        <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i == 32U)) || ((i == 9 &&
        _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i
        == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || (i == 9 && _he_bkt_i
        == 128U)) || (6 <= i && i <= 9)) || i == 5) || i == 4) || i == 3) || i ==
        2) || i == 1)) || (((((((0 == i && 0 == users) && 0 == altusers) && i == 0)
        && i == users) && i == altusers) && users == 0) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 3631
        function: main
      value: ((((4UL == _hj_k && users == altusers) && _hj_k == _hj_k) && _hj_k ==
        4U) && ((((((((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <= 9) && (_he_bkt_i
        == 64U || _he_bkt_i == 32U)) || (i == 9 && _he_bkt_i == 128U)) || (8 <= i
        && i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((8
        <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || ((8 <= i &&
        i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U) && _he_bkt_i
        == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (i ==
        9 && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i
        == 32U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((7 <=
        i && i <= 9) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i ==
        32U)) || (i == 9 && _he_bkt_i == 128U)) || (6 <= i && i <= 9)) || i == 5)
        || i == 4) || i == 3) || i == 2) || i == 1)) || (((((0 == i && 0 == altusers)
        && i == 0) && i == altusers) && user == users) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4214
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4214
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4214
        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_FNV_test5-1.i
        line: 744
        column: 4214
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4214
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4214
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4214
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4214
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4214
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 4214
        function: main
      value: (((((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <= 9) && ((_he_bkt_i
        == 64U || _he_bkt_i == 32U) || _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 256U)) || (8 <= i && i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U))
        || ((7 <= i && i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U))
        || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i == 32U))
        || (((8 <= i && i <= 9) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((i
        == 9 && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) &&
        _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _he_bkt_i == 32U)) || ((8 <=
        i && i <= 9) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i == 256U)) || (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_FNV_test5-1.i
        line: 744
        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_FNV_test5-1.i
        line: 744
        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_FNV_test5-1.i
        line: 744
        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_FNV_test5-1.i
        line: 744
        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_FNV_test5-1.i
        line: 744
        column: 39
        function: main
      value: ((((4UL == _hj_k && users == altusers) && _hj_k == _hj_k) && _hj_k ==
        4U) && (((((((((((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <= 9) && ((_he_bkt_i
        == 64U || _he_bkt_i == 32U) || _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 256U)) || (8 <= i && i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U))
        || ((7 <= i && i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U))
        || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i == 32U))
        || (((8 <= i && i <= 9) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((i
        == 9 && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) &&
        _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _he_bkt_i == 32U)) || ((8 <=
        i && i <= 9) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i == 256U)) || (6
        <= i && i <= 9)) || i == 5) || i == 4) || i == 3) || i == 2) || i == 1)) ||
        (((((0 == i && 0 == altusers) && i == 0) && i == altusers) && user == users)
        && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: 0x9e3779b9u == _hj_i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: 0x9e3779b9u == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: 0xfeedbeefu == _hf_hashv
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hf_hashv == 4276993775U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hj_i == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hj_i == _hj_j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hj_j == 2654435769U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: _hj_key == & j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: (void *)_hj_key == (void *)(& j)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 216
        function: main
      value: ((((0 == i && count_int_int == 0) && i == 0) && j == 0) && *((int *)_hj_key)
        == 0) || ((((((1 <= count_int_int && 2 <= i) && 4 <= j) && 4 <= *((int *)_hj_key))
        && i <= 9) && j <= 81) && *((int *)_hj_key) <= 81)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3663
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3663
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3663
        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_FNV_test5-1.i
        line: 744
        column: 3663
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3663
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3663
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3663
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3663
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3663
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3663
        function: main
      value: (((((((((((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <= 9) && ((_he_bkt_i
        == 64U || _he_bkt_i == 32U) || _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 256U)) || (8 <= i && i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U))
        || ((7 <= i && i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U))
        || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i == 32U))
        || (((8 <= i && i <= 9) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((i
        == 9 && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) &&
        _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _he_bkt_i == 32U)) || ((8 <=
        i && i <= 9) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i == 256U)) || (6
        <= i && i <= 9)) || i == 5) || i == 4) || i == 3) || i == 2) || i == 1) ||
        (((0 == i && i == 0) && user == users) && user == altusers)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2471
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2471
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2471
        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_FNV_test5-1.i
        line: 744
        column: 2471
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2471
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2471
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2471
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2471
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 2471
        function: main
      value: (users == altusers && (((((((((((((((((((((_he_bkt_i == 64U && ((((8
        <= i && i <= 9) && ((_he_bkt_i == 64U || _he_bkt_i == 32U) || _he_bkt_i ==
        128U)) || (i == 9 && _he_bkt_i == 256U)) || (8 <= i && i <= 9))) || ((i ==
        9 && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i
        == 64U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i == 64U))
        || ((i == 9 && _he_bkt_i == 32U) && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i
        == 128U) && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i
        == 128U)) || (i == 9 && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i
        == 32U) && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i == 128U)
        && _he_bkt_i == 32U)) || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i == 32U))
        || ((7 <= i && i <= 9) && _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _he_bkt_i
        == 32U)) || ((8 <= i && i <= 9) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 256U)) || (6 <= i && i <= 9)) || i == 5) || i == 4) || i == 3) || i ==
        2) || i == 1)) || (((((0 == i && 0 == altusers) && i == 0) && i == altusers)
        && user == users) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 39
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 39
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 39
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 39
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 39
        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_FNV_test5-1.i
        line: 748
        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_FNV_test5-1.i
        line: 748
        column: 39
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 39
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 39
        function: main
      value: (((0 == i && count_int_int == 0) && i == 0) && j == 0) || ((((((((((((1
        <= count_int_int && 2 <= i) && 4 <= j) && 4 <= *((int *)_hj_key)) && i <=
        9) && j <= 81) && *((int *)_hj_key) <= 81) && 4UL == _hj_k) && _hj_k == _hj_k)
        && _hj_k == _hj_k) && _hj_k == 4U) && _hj_key == & j) && (void *)_hj_key ==
        (void *)(& j))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3721
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3721
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3721
        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_FNV_test5-1.i
        line: 744
        column: 3721
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3721
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3721
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3721
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3721
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3721
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3721
        function: main
      value: (((((((((((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <= 9) && ((_he_bkt_i
        == 64U || _he_bkt_i == 32U) || _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 256U)) || (8 <= i && i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U))
        || ((7 <= i && i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U))
        || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i == 32U))
        || (((8 <= i && i <= 9) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((i
        == 9 && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) &&
        _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _he_bkt_i == 32U)) || ((8 <=
        i && i <= 9) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i == 256U)) || (6
        <= i && i <= 9)) || i == 5) || i == 4) || i == 3) || i == 2) || i == 1) ||
        (((0 == i && i == 0) && user == users) && user == altusers)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 3578
        function: main
      value: ((((4UL == _hj_k && users == altusers) && _hj_k == _hj_k) && _hj_k ==
        4U) && ((((((((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <= 9) && (_he_bkt_i
        == 64U || _he_bkt_i == 32U)) || (i == 9 && _he_bkt_i == 128U)) || (8 <= i
        && i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i == 128U)) || (((8
        <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U)) || ((8 <= i &&
        i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U) && _he_bkt_i
        == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U)) || (i ==
        9 && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i
        == 32U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((7 <=
        i && i <= 9) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i ==
        32U)) || (i == 9 && _he_bkt_i == 128U)) || (6 <= i && i <= 9)) || i == 5)
        || i == 4) || i == 3) || i == 2) || i == 1)) || (((((0 == i && 0 == altusers)
        && i == 0) && i == altusers) && user == users) && altusers == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5042
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5042
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5042
        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_FNV_test5-1.i
        line: 744
        column: 5042
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5042
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5042
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5042
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5042
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5042
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 5042
        function: main
      value: ((((((((((((((((i <= 9 && (((_he_bkt_i == 64U && ((8 <= i && _he_bkt_i
        <= 127U) || (7 <= i && _he_bkt_i <= 63U))) || ((8 <= i && _he_bkt_i <= 127U)
        && _he_bkt_i == 32U)) || ((8 <= i && _he_bkt_i <= 127U) && _he_bkt_i == 128U)))
        || ((_he_bkt_i <= 127U && i == 9) && _he_bkt_i == 256U)) || ((8 <= i && i
        <= 9) && _he_bkt_i <= 127U)) || (((7 <= i && i <= 9) && _he_bkt_i <= 63U)
        && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i <= 63U) && _he_bkt_i
        == 128U)) || ((_he_bkt_i <= 63U && i == 9) && _he_bkt_i == 256U)) || ((7 <=
        i && i <= 9) && _he_bkt_i <= 63U)) || ((_he_bkt_i <= 255U && i == 9) && _he_bkt_i
        == 64U)) || (((7 <= i && i <= 9) && _he_bkt_i <= 31U) && _he_bkt_i == 64U))
        || ((_he_bkt_i <= 255U && i == 9) && _he_bkt_i == 32U)) || ((_he_bkt_i <=
        255U && i == 9) && _he_bkt_i == 128U)) || ((_he_bkt_i <= 255U && i == 9) &&
        _he_bkt_i == 256U)) || (_he_bkt_i <= 255U && i == 9)) || (((6 <= i && i <=
        9) && _he_bkt_i <= 31U) && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i
        <= 31U) && _he_bkt_i == 128U)) || ((_he_bkt_i <= 31U && i == 9) && _he_bkt_i
        == 256U)) || ((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_FNV_test5-1.i
        line: 744
        column: 3809
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3809
        function: main
      value: 4UL == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3809
        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_FNV_test5-1.i
        line: 744
        column: 3809
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3809
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3809
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3809
        function: main
      value: _hj_key == & user->id
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3809
        function: main
      value: _hj_k == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3809
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 744
        column: 3809
        function: main
      value: (((((((((((((((((((((_he_bkt_i == 64U && ((((8 <= i && i <= 9) && ((_he_bkt_i
        == 64U || _he_bkt_i == 32U) || _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 256U)) || (8 <= i && i <= 9))) || ((i == 9 && _he_bkt_i == 64U) && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 64U) && _he_bkt_i == 32U))
        || ((7 <= i && i <= 9) && _he_bkt_i == 64U)) || ((i == 9 && _he_bkt_i == 32U)
        && _he_bkt_i == 128U)) || ((i == 9 && _he_bkt_i == 128U) && _he_bkt_i == 128U))
        || ((i == 9 && _he_bkt_i == 256U) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i
        == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i == 32U) && _he_bkt_i == 32U))
        || (((8 <= i && i <= 9) && _he_bkt_i == 128U) && _he_bkt_i == 32U)) || ((i
        == 9 && _he_bkt_i == 256U) && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) &&
        _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _he_bkt_i == 32U)) || ((8 <=
        i && i <= 9) && _he_bkt_i == 128U)) || (i == 9 && _he_bkt_i == 256U)) || (6
        <= i && i <= 9)) || i == 5) || i == 4) || i == 3) || i == 2) || i == 1) ||
        (((0 == i && i == 0) && user == users) && user == altusers)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        function: main
      value: 0 <= j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        function: main
      value: j <= 81
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2516
        function: main
      value: '*((int *)_hj_key) <= 81'
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        function: main
      value: _hj_key == & user->cookie
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2516
        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_FNV_test5-1.i
        line: 748
        column: 2516
        function: main
      value: _hj_key == & j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 748
        column: 2516
        function: main
      value: (void *)_hj_key == (void *)(& j)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4912
        function: main
      value: users == altusers
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4912
        function: main
      value: _hj_k == _hj_k
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/uthash-2.0.2/uthash_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        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_FNV_test5-1.i
        line: 743
        column: 4912
        function: main
      value: ((((((((((((_he_bkt_i == 64U && (((8 <= i && i <= 9) && ((_he_bkt_i <=
        63U || _he_bkt_i <= 127U) || _he_bkt_i <= 31U)) || (_he_bkt_i <= 255U && i
        == 9))) || ((_he_bkt_i <= 63U && i == 9) && _he_bkt_i == 128U)) || ((_he_bkt_i
        <= 127U && i == 9) && _he_bkt_i == 128U)) || (((7 <= i && i <= 9) && _he_bkt_i
        <= 63U) && _he_bkt_i == 32U)) || (((8 <= i && i <= 9) && _he_bkt_i <= 127U)
        && _he_bkt_i == 32U)) || ((7 <= i && i <= 9) && _he_bkt_i <= 63U)) || ((8
        <= i && i <= 9) && _he_bkt_i <= 127U)) || ((_he_bkt_i <= 31U && i == 9) &&
        _he_bkt_i == 128U)) || ((_he_bkt_i <= 255U && i == 9) && _he_bkt_i == 128U))
        || (((7 <= i && i <= 9) && _he_bkt_i <= 31U) && _he_bkt_i == 32U)) || ((_he_bkt_i
        <= 255U && i == 9) && _he_bkt_i == 32U)) || ((6 <= i && i <= 9) && _he_bkt_i
        <= 31U)) || (_he_bkt_i <= 255U && i == 9)
      format: c_expression
