- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: b34d76c4-3060-4e3d-8848-d2dcfc707666
    creation_time: 2025-03-22T11:31:24Z
    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/weaver/chl-poker-hand-subst.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c: 6f5429be3277265830db62d0e901249d8c763b3d6d062789dc5a6193a05c0714
      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/weaver/chl-poker-hand-subst.wvr.c
        line: 170
        column: 5
        function: thread2
      value: (unsigned int )_argptr == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 142
        column: 5
        function: thread2
      value: (unsigned int )_argptr == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: last_index_of_11 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: result_12 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: i1_13 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: i2_15 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: result_17 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: i1_18 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: i2_20 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: result_22 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: i1_23 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: i2_25 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: break_14 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: break_16 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: break_19 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: break_21 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: break_24 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: break_26 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 354
        column: 3
        function: create_fresh_int_array
      value: (((((((((((4 == size && size == 4) && i == 4) || (((((((((4 <= i && i
        <= 13) && 13 == size) && count_occurrences_of_2 == 0) && last_index_of_3 ==
        0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0) && char_at_9 ==
        0) && count_occurrences_of_10 == 0) && size == 13)) || (((((((((((4 <= i &&
        i <= 13) && 13 == size) && char_at_1 == 0) && count_occurrences_of_2 == 0)
        && last_index_of_3 == 0) && char_at_5 == 0) && count_occurrences_of_6 == 0)
        && last_index_of_7 == 0) && char_at_9 == 0) && count_occurrences_of_10 ==
        0) && size == 13)) || ((((((((((4 <= i && i <= 13) && 13 == size) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 13)) || ((((((((((((4 <= i && i <= 5) && 5 == size) && char_at_1
        == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && char_at_5
        == 0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0) && index_of_8
        == 0) && char_at_9 == 0) && count_occurrences_of_10 == 0) && size == 5)) ||
        (((((((((((((4 <= i && i <= 5) && 5 == size) && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && index_of_4 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 5)) || ((((((((((((((4 <= i && i <= 5) && 5 == size) && index_of_0
        == 0) && char_at_1 == 0) && count_occurrences_of_2 == 0) && last_index_of_3
        == 0) && index_of_4 == 0) && char_at_5 == 0) && count_occurrences_of_6 ==
        0) && last_index_of_7 == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 5)) || (i == 3 && (((((((4 == size && size == 4) || (((((((13
        == size && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 13)) || (((((((((13 == size && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 13)) || ((((((((13 == size && count_occurrences_of_2 == 0)
        && last_index_of_3 == 0) && char_at_5 == 0) && count_occurrences_of_6 == 0)
        && last_index_of_7 == 0) && char_at_9 == 0) && count_occurrences_of_10 ==
        0) && size == 13)) || ((((((((((5 == size && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 5)) || (((((((((((5 == size && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && index_of_4 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 5)) || ((((((((((((5 == size && index_of_0 == 0) && char_at_1
        == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && index_of_4
        == 0) && char_at_5 == 0) && count_occurrences_of_6 == 0) && last_index_of_7
        == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10 ==
        0) && size == 5)))) || (i == 2 && (((((((4 == size && size == 4) || (((((((13
        == size && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 13)) || (((((((((13 == size && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 13)) || ((((((((13 == size && count_occurrences_of_2 == 0)
        && last_index_of_3 == 0) && char_at_5 == 0) && count_occurrences_of_6 == 0)
        && last_index_of_7 == 0) && char_at_9 == 0) && count_occurrences_of_10 ==
        0) && size == 13)) || ((((((((((5 == size && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 5)) || (((((((((((5 == size && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && index_of_4 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 5)) || ((((((((((((5 == size && index_of_0 == 0) && char_at_1
        == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && index_of_4
        == 0) && char_at_5 == 0) && count_occurrences_of_6 == 0) && last_index_of_7
        == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10 ==
        0) && size == 5)))) || (i == 1 && (((((((4 == size && size == 4) || (((((((13
        == size && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 13)) || (((((((((13 == size && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 13)) || ((((((((13 == size && count_occurrences_of_2 == 0)
        && last_index_of_3 == 0) && char_at_5 == 0) && count_occurrences_of_6 == 0)
        && last_index_of_7 == 0) && char_at_9 == 0) && count_occurrences_of_10 ==
        0) && size == 13)) || ((((((((((5 == size && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 5)) || (((((((((((5 == size && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && index_of_4 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 5)) || ((((((((((((5 == size && index_of_0 == 0) && char_at_1
        == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && index_of_4
        == 0) && char_at_5 == 0) && count_occurrences_of_6 == 0) && last_index_of_7
        == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10 ==
        0) && size == 5)))) || ((0 == i && i == 0) && (((((((4 == size && size ==
        4) || (((((((13 == size && count_occurrences_of_2 == 0) && last_index_of_3
        == 0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0) && char_at_9
        == 0) && count_occurrences_of_10 == 0) && size == 13)) || (((((((((13 == size
        && char_at_1 == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0)
        && char_at_5 == 0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0)
        && char_at_9 == 0) && count_occurrences_of_10 == 0) && size == 13)) || ((((((((13
        == size && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && char_at_5
        == 0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0) && char_at_9
        == 0) && count_occurrences_of_10 == 0) && size == 13)) || ((((((((((5 == size
        && char_at_1 == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0)
        && char_at_5 == 0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0)
        && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10 == 0) &&
        size == 5)) || (((((((((((5 == size && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && index_of_4 == 0) && char_at_5 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10
        == 0) && size == 5)) || ((((((((((((5 == size && index_of_0 == 0) && char_at_1
        == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && index_of_4
        == 0) && char_at_5 == 0) && count_occurrences_of_6 == 0) && last_index_of_7
        == 0) && index_of_8 == 0) && char_at_9 == 0) && count_occurrences_of_10 ==
        0) && size == 5)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 86
        column: 5
        function: thread1
      value: (unsigned int )_argptr == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-subst.wvr.c
        line: 57
        column: 5
        function: thread1
      value: (unsigned int )_argptr == 0U
      format: c_expression
