- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 863c774f-c19d-4cf2-a344-127929476842
    creation_time: 2025-03-22T11:33:52Z
    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/libvsync/semaphore.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i: c654263c1c366ef9cc67f02592c2d3fd912134a9cb5af429926a9f4627826820
      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/libvsync/semaphore.i
        line: 5976
        column: 10
        function: reader_cs
      value: tid == 2U || tid == 3U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 6019
        column: 5
        function: main
      value: i == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 6019
        column: 5
        function: main
      value: i == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 6019
        column: 5
        function: main
      value: (((i == 4U || i == 3U) || i == 2U) || i == 1U) || (0 == i && i == 0U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 4812
        column: 5
        function: vatomic32_await_neq
      value: c <= 3U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 4812
        column: 5
        function: vatomic32_await_neq
      value: (void *)a == (void *)(& g_semaphore.s)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 6053
        column: 10
        function: reader_release
      value: tid == 2U || tid == 3U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 6010
        column: 5
        function: main
      value: (i == 2U || i == 1U) || (0 == i && i == 0U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 6041
        column: 10
        function: writer_release
      value: tid == 0U || tid == 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5978
        column: 5
        function: reader_cs
      value: tid == 2U || tid == 3U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5978
        column: 5
        function: reader_cs
      value: a == 0U || a == 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 6014
        column: 5
        function: main
      value: i == 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 6014
        column: 5
        function: main
      value: ((2 == i && i == 2U) || i == 4U) || i == 3U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 6047
        column: 10
        function: reader_acquire
      value: tid == 2U || tid == 3U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 4813
        column: 9
        function: vatomic32_await_neq
      value: c <= 3U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 4813
        column: 9
        function: vatomic32_await_neq
      value: (void *)a == (void *)(& g_semaphore.s)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5969
        column: 10
        function: writer_cs
      value: tid == 0U || tid == 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 573
        column: 10
        function: verification_loop_bound
      value: (bound == 3U && bound == (vuint32_t )3) || (bound == 5U && bound == (vuint32_t
        )5)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 568
        column: 10
        function: verification_spin_end
      value: v == 0 || v == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 6035
        column: 10
        function: writer_acquire
      value: tid == 0U || tid == 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5038
        column: 9
        function: vatomic32_await_ge_sub
      value: a == & g_semaphore.s
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5038
        column: 9
        function: vatomic32_await_ge_sub
      value: c == v
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5038
        column: 9
        function: vatomic32_await_ge_sub
      value: c == 1U || c == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5038
        column: 9
        function: vatomic32_await_ge_sub
      value: v == 1U || v == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5036
        column: 5
        function: vatomic32_await_ge_sub
      value: a == & g_semaphore.s
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5036
        column: 5
        function: vatomic32_await_ge_sub
      value: c == v
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5036
        column: 5
        function: vatomic32_await_ge_sub
      value: 1U <= cur || (0 == cur && cur == 0U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5036
        column: 5
        function: vatomic32_await_ge_sub
      value: c == 1U || c == 4U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/libvsync/semaphore.i
        line: 5036
        column: 5
        function: vatomic32_await_ge_sub
      value: v == 1U || v == 4U
      format: c_expression
