- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 0b57ca84-8411-465a-aa94-77702e7039d5
    creation_time: 2025-03-22T11:31:27Z
    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-symm.wvr.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c: 6f8a234fc2a7dd634bd03f872a0d7e8707283ecf0f996c6ed729f53ab07d6660
      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-symm.wvr.c
        line: 139
        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-symm.wvr.c
        line: 55
        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-symm.wvr.c
        line: 83
        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-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: char_at_5 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: result_8 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: i1_9 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: i2_11 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: result_13 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: i1_14 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: i2_16 == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: break_10 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: break_12 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: break_15 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: break_17 == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 245
        column: 3
        function: create_fresh_int_array
      value: ((((((((((char_at_1 == 0 && last_index_of_3 == 0) && last_index_of_7
        == 0) && ((((((((4 <= i && i <= 5) && 5 == size) && index_of_0 == 0) && count_occurrences_of_2
        == 0) && index_of_4 == 0) && count_occurrences_of_6 == 0) && size == 5) ||
        ((4 == size && size == 4) && i == 4))) || ((4 <= i && i <= 13) && (size ==
        4 || size == 13))) || (((((((4 == size && char_at_1 == 0) && count_occurrences_of_2
        == 0) && last_index_of_3 == 0) && count_occurrences_of_6 == 0) && last_index_of_7
        == 0) && size == 4) && i == 4)) || ((((((4 == size && char_at_1 == 0) && last_index_of_3
        == 0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0) && size ==
        4) && i == 4)) || (((((((((4 <= i && i <= 5) && 5 == size) && char_at_1 ==
        0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && index_of_4
        == 0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0) && size ==
        5)) || (i == 3 && (((((((char_at_1 == 0 && last_index_of_3 == 0) && last_index_of_7
        == 0) && ((((((5 == size && index_of_0 == 0) && count_occurrences_of_2 ==
        0) && index_of_4 == 0) && count_occurrences_of_6 == 0) && size == 5) || (4
        == size && size == 4))) || (size == 4 || size == 13)) || ((((((4 == size &&
        char_at_1 == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) &&
        count_occurrences_of_6 == 0) && last_index_of_7 == 0) && size == 4)) || (((((4
        == size && char_at_1 == 0) && last_index_of_3 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && size == 4)) || (((((((5 == size && char_at_1
        == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && index_of_4
        == 0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0) && size ==
        5)))) || (i == 2 && (((((((char_at_1 == 0 && last_index_of_3 == 0) && last_index_of_7
        == 0) && ((((((5 == size && index_of_0 == 0) && count_occurrences_of_2 ==
        0) && index_of_4 == 0) && count_occurrences_of_6 == 0) && size == 5) || (4
        == size && size == 4))) || (size == 4 || size == 13)) || ((((((4 == size &&
        char_at_1 == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) &&
        count_occurrences_of_6 == 0) && last_index_of_7 == 0) && size == 4)) || (((((4
        == size && char_at_1 == 0) && last_index_of_3 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && size == 4)) || (((((((5 == size && char_at_1
        == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && index_of_4
        == 0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0) && size ==
        5)))) || (i == 1 && (((((((char_at_1 == 0 && last_index_of_3 == 0) && last_index_of_7
        == 0) && ((((((5 == size && index_of_0 == 0) && count_occurrences_of_2 ==
        0) && index_of_4 == 0) && count_occurrences_of_6 == 0) && size == 5) || (4
        == size && size == 4))) || (size == 4 || size == 13)) || ((((((4 == size &&
        char_at_1 == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) &&
        count_occurrences_of_6 == 0) && last_index_of_7 == 0) && size == 4)) || (((((4
        == size && char_at_1 == 0) && last_index_of_3 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && size == 4)) || (((((((5 == size && char_at_1
        == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && index_of_4
        == 0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0) && size ==
        5)))) || ((0 == i && i == 0) && (((((((char_at_1 == 0 && last_index_of_3 ==
        0) && last_index_of_7 == 0) && ((((((5 == size && index_of_0 == 0) && count_occurrences_of_2
        == 0) && index_of_4 == 0) && count_occurrences_of_6 == 0) && size == 5) ||
        (4 == size && size == 4))) || (size == 4 || size == 13)) || ((((((4 == size
        && char_at_1 == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0)
        && count_occurrences_of_6 == 0) && last_index_of_7 == 0) && size == 4)) ||
        (((((4 == size && char_at_1 == 0) && last_index_of_3 == 0) && count_occurrences_of_6
        == 0) && last_index_of_7 == 0) && size == 4)) || (((((((5 == size && char_at_1
        == 0) && count_occurrences_of_2 == 0) && last_index_of_3 == 0) && index_of_4
        == 0) && count_occurrences_of_6 == 0) && last_index_of_7 == 0) && size ==
        5)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/weaver/chl-poker-hand-symm.wvr.c
        line: 167
        column: 5
        function: thread2
      value: (unsigned int )_argptr == 0U
      format: c_expression
