- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab4bbc7a-eaa7-4698-8f8e-9603162f7634
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05bb85b1-9066-478b-b32d-0b62b54a1dfe
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c72f8896-41d4-4a32-be77-d0140d9353cd
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa7d89a3-f2ea-4765-a202-a9a5d137055e
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8d1193b-5be4-4672-bdc5-facc1280c990
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff0 == 0 || z$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ee496fc-4fdf-452a-8498-0118a4be0892
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff0 == 0 || z$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd4f27ca-3572-4047-86d7-11e4d16c8bc7
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff0 == 0 || z$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34bd2435-3948-43c3-91b1-90e62cd03be6
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff0 == 0 || z$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24f207d2-6938-4963-9b41-0026804f570b
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$mem_tmp == 0 || z$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 500a3633-e189-4601-bb22-298669754bd5
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$mem_tmp == 0 || z$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3fb96a2-85b1-45a3-b4e4-7582831837bd
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$mem_tmp == 0 || z$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71dc2d87-ce3e-489b-85de-753eae3093d8
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$mem_tmp == 0 || z$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d4d907f-e08d-4a5c-8363-7dba8c5ce7cf
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58f7e8c7-fef8-4b62-b2b0-18d9be233cfa
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f640fdc-e4f2-4046-bb6c-e117133844de
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27dd7f78-651a-459f-b4a6-84d334a949fa
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51b9b8d9-4b76-40ca-891d-b3b988348e15
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 130d6f33-12a0-4ccb-9ea5-5094b0e2c475
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b795d339-86d8-4c4a-bc92-1e3f904dee72
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fc2b636-6121-4a35-8640-f99f306827ca
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b048947-4599-42f8-ac06-1cd6d5565be8
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 42da20c7-6231-4831-b94a-90302a9d0ef2
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8d614dc-87f7-4772-952a-ecf1cbe34161
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9762b37d-edfc-4690-b075-1d7932ad9080
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 046d7a89-94cc-44b4-ae36-f11c5142768a
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    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: ffd6f1e3-a6a9-4191-86cd-023e5331f10e
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    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: 4da70915-6aa3-49cc-87eb-1dc73bc51fd0
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    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: b1a11213-2697-4795-9180-e4e2d2c4c93f
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    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: 2bff5fed-e8b4-49a0-862d-4806dbceb341
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x == 0 || x == 1) || x == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fcf6b6be-e88b-44d1-837f-1bc8056b66a5
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x == 0 || x == 1) || x == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97424837-ce9b-48bf-8bd4-c53f67593f1b
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x == 0 || x == 1) || x == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f78e294d-1c8b-46d1-8dad-c553a359943b
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x == 0 || x == 1) || x == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32e91210-0a3b-4342-b3b4-330916bbcd2d
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y == 0 || y == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5a65280-290a-438b-ad50-83814cc82734
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y == 0 || y == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55a273a9-ec5c-4575-b95e-d21a60f5925b
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y == 0 || y == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ceaeef87-8b83-4661-a31f-7de6d05d2c90
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y == 0 || y == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 547c818a-e9f1-4ac9-8e9b-9efb27f73a76
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87c2d500-f9cc-431c-bd08-a9a6e98a5e73
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38dd9d4a-0faa-43ad-a58a-1f2987f8d655
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 092d16ce-8f07-4023-9957-52982b52388e
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 132b5ff9-8aff-4479-b86c-784c643d7b05
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    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: 159ea801-7d8b-4041-b260-499586d618ec
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    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: 261f35aa-980c-4a61-9897-b70d3ff89663
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    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: 765f5ea0-cc10-495b-87ad-00351e647c17
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    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: 441aeac1-06a8-4de7-a15f-2d34d7e757bb
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    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: 2bf8eebc-1973-4a37-89ee-d93fb7472d87
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    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: 053d2da7-b6e2-4b69-98aa-7c653dd68af4
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    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: c88106a4-879a-43cf-9f18-2a3d8840c1fc
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    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: adaeff2f-1802-43ac-a7a0-b520814262b2
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d34020c9-6e08-4c5f-9e57-309234f9f873
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9744570a-aaf1-4df0-b65d-fa818b7f6765
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60e6ff0e-83ee-4f21-9286-eb875217b4bc
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36255b0e-bab8-4fff-8e16-2cf130536529
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c3137e87-1a13-4b11-9c1f-52e25722beeb
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 335c8069-7b10-4f87-9ac5-02e6be198898
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: accc79a2-47c8-47c0-9dce-358c2e18f1ef
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 366cce48-5eca-483d-b798-cb1c1542a512
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71a2520a-9de2-4273-b82d-6b84c3c10c47
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 743ed3db-acf5-4fce-8ed2-e23b9f6cc32d
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0cd8ffe9-2b80-4046-a2bb-c836a0944a0a
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c2ce30a-cb88-4bb9-add2-4017fafbe232
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    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: 18dddac8-766b-408d-8ea5-c2535ab5ee93
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    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: 54d69937-efbc-4470-bbe4-b5c3eae2d2d1
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    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: d5378d8a-5c0b-4902-b1b4-0e6b5ebefeec
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    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: d95ade0e-59e6-40fa-accb-47ba2a05e18a
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff1 == 0 || z$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e789f57a-5310-4373-8af1-822b7ae2c838
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff1 == 0 || z$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffd62b35-74ab-43d8-8899-be3d015911ea
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff1 == 0 || z$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e9fc774-3ba5-4bee-980e-37a0ba040c6d
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff1 == 0 || z$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5336906f-737c-40a6-8d1c-2804a877df31
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    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: 5010e2b1-e482-4553-a72f-ee35537b498c
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    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: 03c5c1ca-865e-4f65-b314-af1f6cdc0c35
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    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: 7ab71206-557e-4529-9026-518beb7e15ad
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    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: e115f3d7-4d97-43bf-9219-6e2af4732095
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bc02f4b-8e84-4ae1-a71f-5bccf919638c
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3a474d9-929b-4d89-b127-8b147be6f594
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a58c2156-69c8-499d-81b0-ca025af315de
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c16296e-18d2-4540-b978-e1a48e91e5a4
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa0be3ae-2bbe-41e2-9eee-3c4b27aa96d5
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 214ca342-5198-4ab9-9b5c-ce75d4723b61
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71cb26da-33ac-43eb-a7aa-acebc7d29d2b
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af9cf59e-89f7-4619-85c2-89be7a065e07
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f5afb82-1380-4ad2-bd7d-77b31ca7038f
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8295bd48-6ba7-458f-a63e-23df6360ac3b
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3bae7d0-597a-4264-8445-2c11e3b077bc
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8954467-da27-4b34-b171-f37e56e8e060
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e06d048-5ec2-4b6b-855b-37032693d35c
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45b87e01-06be-423b-983a-c2241c7dd258
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 821d4373-72cd-43de-848b-617c0c09a5c1
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: e89a8d38-c17b-4335-a35a-e4db65cd7839
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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: cd87101a-0c80-4984-9eb6-48ce199f4944
    creation_time: 2024-07-04T11:36:15Z
    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/mix051_pso.opt_rmo.opt_tso.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix051_pso.opt_rmo.opt_tso.opt.i: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
      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/mix051_pso.opt_rmo.opt_tso.opt.i
    file_hash: 0f6a99f321ab4c9a330ddab5bc184070524e662cb34c3dfc8d7fb0257fb493dd
    line: 847
    column: 3
    function: main
