- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e76a5d8-63f1-4b35-9821-6606eba090bf
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$w_buff0 == 0 || b$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5ed2ced-87e6-409c-ba6a-0d1573bdeb2d
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$w_buff0 == 0 || b$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83a2e0d4-7e60-4704-9e6f-bb11bc8586a6
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$w_buff0 == 0 || b$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 595ea66a-b3a5-4b27-ba53-a4baf63439c5
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$w_buff0 == 0 || b$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2fd43ad-3bb5-4f9e-aa5c-65a153bb0865
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z == 0 || z == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 790d7e7b-8df0-4c1a-b20f-227f48a445cb
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z == 0 || z == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e498e88-8ff3-4722-a12e-77a71d881a90
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z == 0 || z == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65f0951c-023d-42f9-9339-c33610d83c8d
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z == 0 || z == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdbf6908-cae6-4158-b9b6-7cde60615038
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b == 0 || b == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b12493e-85c2-43f1-a1fd-67bea4ada1e0
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b == 0 || b == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf62e799-cf06-40b6-adb1-cb08bbc02c63
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b == 0 || b == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56db993e-716f-4bb4-b5ae-5626fac20a08
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b == 0 || b == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9b86653-d174-4909-82fa-003aa134a24b
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a == 0 || a == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d328f44-6ff6-4e27-a071-f8fef548c2b6
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a == 0 || a == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99eb0964-730f-4d42-bc1d-8bffacb11a26
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a == 0 || a == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b362735-4efe-4bc9-8ee1-27a15123cc09
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (a == 0 || a == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fee1544-f0d7-439c-92de-282afa6f5086
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6eaca5e1-6a8d-4670-8c9f-e663ccde2e8a
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70f8ee16-bba3-4e43-bd0b-38400ad9712e
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 970bfaa5-fc75-4888-9825-73ffd159482e
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2fc970c8-70cc-4245-8e71-77f7c138a38d
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (x == 0 || x == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6886da4-052e-48d5-89ff-c9e39ce8dab4
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (x == 0 || x == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1de53b3a-5f85-46f2-b99e-2ec1d8eb3602
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (x == 0 || x == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 473f61b5-7d1a-4ce9-9864-8e94401b1d18
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (x == 0 || x == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bcbc00bb-67e5-434d-bf2c-9c2301810ec1
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 071aa209-7f09-4f01-a51a-016dd22410f8
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57645367-176f-4096-9052-f4e8c29ad5cb
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b57b5f3b-7945-4239-9ae4-56fdf9393223
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5961e007-50c9-49b0-b3fe-6b536b0df962
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0fab760-fa04-4b12-8989-522b6f670c6f
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b423696d-b976-4b3f-8c8d-5836fef5742f
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b8a71d0-8a6e-444b-bdf0-80ffdb391060
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9804df7-6981-4338-aa17-3990efdcb577
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9b016de-dae4-4129-bb18-7406bd423bfc
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b62440c-dffa-4cec-a2b4-57403f875983
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae1f5e52-629d-4ab2-ba26-a1508ad32c30
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b8955d2-a272-4780-a0d3-77aa5f7d48f6
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce9300b2-a1e0-426e-85dd-622cb31bcda7
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8dbcd33-fa92-452b-bd4e-d8321173bb12
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06d9b5dc-00e0-4487-95d9-507583810120
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: def6baf8-5c49-4b22-a668-4d1024bf41ae
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01a7e51e-d9d4-438b-a6ef-f5d22497b2b9
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56bad9f5-13c4-4127-a493-f363afb1c0bf
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 407723b4-fd81-4cdf-adb8-1900cd3fe12a
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99582b86-b6b2-4a67-8112-074a0b1b5d0d
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e750408-b8b0-4ed9-97b5-37e518d8b806
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a33ffe3d-5958-41a7-8583-ea73f2204254
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e3790c2-4958-45ae-b4ac-4c314f73221b
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c4d8109-5cba-4161-87f1-264b460f3857
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((y == 0 || y == 1) || y == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c9bb971-71b6-4ae9-aa4b-5a0dca8ca7df
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((y == 0 || y == 1) || y == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef03a75f-590b-4013-8090-03cf9588672b
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((y == 0 || y == 1) || y == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a04312b-d24d-4439-9420-fee9d9f632c7
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((y == 0 || y == 1) || y == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cfade3ba-18d3-44d5-8848-4e68a8811dac
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b0e0163-4b54-47f7-badc-4b1d5cfe040f
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c92901e-4b03-47d2-8e14-d466be663471
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ccaff10f-526c-4ad8-bb83-bd3b57755ed7
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d154040e-bc57-4131-a70f-4300a9db7e9c
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 126bb967-5d89-40d0-9a55-389f121f452e
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aefea297-f73b-436e-99c5-1f0698c196c3
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ef922b4-6abb-4dc5-ae3c-7b48235b59b3
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6faa18e8-0347-491a-9197-5df1de600c9e
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3275a723-09fd-4322-9ae2-6faa1946ae82
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93db33f2-2652-4041-a6dc-5513e9392770
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f4a6aba-838c-4f38-88a6-d74efeb9afbe
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da3c1f1e-4af7-4681-add4-8789211e1da7
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11567f8b-4426-4d89-8c7f-8f33fbe17f94
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3663b671-fc84-41ad-8587-0450eed232b6
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3f26a38-31ff-4945-9b18-402a8b4b15b6
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bdede9fa-38bd-4dcf-ba7c-8ac1ee746217
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d06e91cd-41a6-4c1c-b849-ac3a3e99e3c1
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24b8e384-a7da-4ef0-a586-72e0f7e2dcd4
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 815139fd-59c6-4e9d-8edb-83745ef03999
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5090370-6cb3-4da0-8bde-f45ea14afc70
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf9197c5-19bd-408a-a00d-5551017a64fb
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50003772-7176-4f36-a6df-941c7b4463ad
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 245477d5-b888-4264-aa16-2eb66aca3fe5
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe1728b9-fc09-4e13-bb27-6a1c8254458c
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 063899ea-4dbe-48ac-a3e1-cae3c9569f14
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c8cb3c9-3a02-48b8-8884-f3dc69406257
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e5eedc3-ca54-4d97-bb96-475dfcc9b918
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 396acb23-42dd-4872-98ba-22681d2e003d
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f6519b7-fb51-44b7-a73f-fb520e11773f
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c136f3f0-71ee-4253-bcd8-8d87855a4f1b
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef95416c-a44c-438f-842c-b3ec8215c83a
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || b$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67a6ebf1-a570-4563-b848-5714866d4c65
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$w_buff1 == 0 || b$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8574e1b-d063-41e8-93a9-e9b4118cc0a9
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$w_buff1 == 0 || b$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df6c490d-2354-4694-9358-0b2b25eda702
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$w_buff1 == 0 || b$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec54154d-6223-4fc5-af22-bcc5c14f9e9a
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$w_buff1 == 0 || b$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 937746b7-84b1-41ad-a653-b951a2e40d9a
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85a750b4-d043-4828-ac29-404f96f359da
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e99473c-7140-407b-b03c-b8c24421c29e
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ccf45df-992b-4499-a98a-865cc717bc4e
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 470f198c-689b-48b1-9e62-4fe5661ca564
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 874
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$mem_tmp == 0 || b$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c39dbdd-c603-489a-9b3a-b15ea81618dd
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$mem_tmp == 0 || b$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95309110-1c93-4344-86b1-64a9d6ce2fdd
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$mem_tmp == 0 || b$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73409a70-4dc1-4333-8019-9b2dafadabfb
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (b$mem_tmp == 0 || b$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 06327b61-69ab-401d-841b-2a254e4484ee
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 870b8982-f299-4a7c-87f2-36c9af7317ca
    creation_time: 2024-07-04T11:36:08Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix039.oepc.i
    file_hash: 42c5ff0d69642601057eb29fc7d78b67af5ab0b43644460199f4561abe049d3b
    line: 872
    column: 3
    function: main
