- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a536ac28-1354-463c-b76c-4b6e829e7e39
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x$w_buff0 == 0 || x$w_buff0 == 1) || x$w_buff0 ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8b70de3-0bee-4b66-ae69-b11e7f708645
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x$w_buff0 == 0 || x$w_buff0 == 1) || x$w_buff0 ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee6b117e-7e58-4aff-ab2c-8014672a066a
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x$w_buff0 == 0 || x$w_buff0 == 1) || x$w_buff0 ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd25cd09-57d9-438f-a8bc-525344be03b0
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40f81308-53f2-4590-b005-0ed7bdb99b70
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a8a66ca-7854-488f-bc05-e50d547e2ad5
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8257b260-b674-4a8b-92bf-dfbc17fa3759
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9db71daf-7afe-4cc7-8cfe-7fad95b796e0
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac0d8327-a52a-4944-915c-26d217557942
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8eacf35f-5985-4f55-bdaf-3d92388f9900
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2c2f659-e2dc-4ab7-b60d-cb512e1eb3ee
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fa729b5-9dba-41f1-afe4-9fff87837d8d
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f08c9e68-63a0-4ed1-b91f-26a43e50495d
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && __unbuffered_p2_EAX$flush_delayed == (_Bool)0) && __unbuffered_p2_EAX$mem_tmp
      == 0) && __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff0 == 0) && __unbuffered_p2_EAX$w_buff0_used
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff1 == 0) && __unbuffered_p2_EAX$w_buff1_used
      == (_Bool)0) && x$flush_delayed == (_Bool)0) && x$r_buff0_thd0 == (_Bool)0)
      && x$r_buff0_thd1 == (_Bool)0) && x$r_buff0_thd3 == (_Bool)0) && x$r_buff1_thd0
      == (_Bool)0) && x$r_buff1_thd1 == (_Bool)0) && x$r_buff1_thd3 == (_Bool)0) &&
      x$read_delayed == (_Bool)0) && x$read_delayed_var == 0) && (__unbuffered_p2_EAX$read_delayed_var
      == 0 || (__unbuffered_p2_EAX$read_delayed_var == & x && ((*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1) || *__unbuffered_p2_EAX$read_delayed_var
      == 2)))) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1)) && (y ==
      0 || y == 1)) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) ||
      __unbuffered_p0_EAX == 2)) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)) && ((x == 0 || x == 1) || x == 2)) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)) && ((x$w_buff0 == 0 || x$w_buff0
      == 1) || x$w_buff0 == 2)) && ((x$w_buff1 == 0 || x$w_buff1 == 1) || x$w_buff1
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35c54908-3676-4799-b8a7-7ecd65aac1ff
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && __unbuffered_p2_EAX$flush_delayed == (_Bool)0) && __unbuffered_p2_EAX$mem_tmp
      == 0) && __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff0 == 0) && __unbuffered_p2_EAX$w_buff0_used
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff1 == 0) && __unbuffered_p2_EAX$w_buff1_used
      == (_Bool)0) && x$flush_delayed == (_Bool)0) && x$r_buff0_thd0 == (_Bool)0)
      && x$r_buff0_thd1 == (_Bool)0) && x$r_buff0_thd3 == (_Bool)0) && x$r_buff1_thd0
      == (_Bool)0) && x$r_buff1_thd1 == (_Bool)0) && x$r_buff1_thd3 == (_Bool)0) &&
      x$read_delayed == (_Bool)0) && x$read_delayed_var == 0) && (__unbuffered_p2_EAX$read_delayed_var
      == 0 || (__unbuffered_p2_EAX$read_delayed_var == & x && ((*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1) || *__unbuffered_p2_EAX$read_delayed_var
      == 2)))) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1)) && (y ==
      0 || y == 1)) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) ||
      __unbuffered_p0_EAX == 2)) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)) && ((x == 0 || x == 1) || x == 2)) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)) && ((x$w_buff0 == 0 || x$w_buff0
      == 1) || x$w_buff0 == 2)) && ((x$w_buff1 == 0 || x$w_buff1 == 1) || x$w_buff1
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d06bfc4-645c-45c2-a161-7d84a0e4ebc7
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && __unbuffered_p2_EAX$flush_delayed == (_Bool)0) && __unbuffered_p2_EAX$mem_tmp
      == 0) && __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff0 == 0) && __unbuffered_p2_EAX$w_buff0_used
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff1 == 0) && __unbuffered_p2_EAX$w_buff1_used
      == (_Bool)0) && x$flush_delayed == (_Bool)0) && x$r_buff0_thd0 == (_Bool)0)
      && x$r_buff0_thd1 == (_Bool)0) && x$r_buff0_thd3 == (_Bool)0) && x$r_buff1_thd0
      == (_Bool)0) && x$r_buff1_thd1 == (_Bool)0) && x$r_buff1_thd3 == (_Bool)0) &&
      x$read_delayed == (_Bool)0) && x$read_delayed_var == 0) && (__unbuffered_p2_EAX$read_delayed_var
      == 0 || (__unbuffered_p2_EAX$read_delayed_var == & x && ((*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1) || *__unbuffered_p2_EAX$read_delayed_var
      == 2)))) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1)) && (y ==
      0 || y == 1)) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) ||
      __unbuffered_p0_EAX == 2)) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)) && ((x == 0 || x == 1) || x == 2)) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)) && ((x$w_buff0 == 0 || x$w_buff0
      == 1) || x$w_buff0 == 2)) && ((x$w_buff1 == 0 || x$w_buff1 == 1) || x$w_buff1
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d23ab2a8-ffe5-44e7-8f5e-93306df724a9
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX$read_delayed_var == 0 || (__unbuffered_p2_EAX$read_delayed_var
      == & x && ((*__unbuffered_p2_EAX$read_delayed_var == 0 || *__unbuffered_p2_EAX$read_delayed_var
      == 1) || *__unbuffered_p2_EAX$read_delayed_var == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 188b17a8-3b4b-46ea-a7e7-c1c961497203
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX$read_delayed_var == 0 || (__unbuffered_p2_EAX$read_delayed_var
      == & x && ((*__unbuffered_p2_EAX$read_delayed_var == 0 || *__unbuffered_p2_EAX$read_delayed_var
      == 1) || *__unbuffered_p2_EAX$read_delayed_var == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 464600b4-5d9e-4037-845d-9a98fc9936e1
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX$read_delayed_var == 0 || (__unbuffered_p2_EAX$read_delayed_var
      == & x && ((*__unbuffered_p2_EAX$read_delayed_var == 0 || *__unbuffered_p2_EAX$read_delayed_var
      == 1) || *__unbuffered_p2_EAX$read_delayed_var == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18456399-079d-4029-bb62-2078b5dd381f
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 056bf470-6a74-4954-8892-9c75bfd34ba8
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5aacaacd-5f44-4a0f-8214-9a4a9a0c22a1
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af8a2b1e-1d8f-4c54-8b0d-b1408db1d15b
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 785036c5-28d2-4b8e-9520-ebcd6f453cef
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b904dc5-a9a0-4581-b97d-c4ec9beae659
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ba6052b-7bd9-401e-b9af-1bfec7ca54b5
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX
      == 1) || __unbuffered_p0_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 982501cb-cf50-4642-bacc-f1f332815787
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX
      == 1) || __unbuffered_p0_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1de3fafc-ab90-4ead-a9be-d74a81916a43
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX
      == 1) || __unbuffered_p0_EAX == 2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 372cad6a-c676-4617-9405-51276ffaa690
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16a2452c-aed4-4efa-9085-6c191d85f750
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4834f2f4-97ea-4cf9-b00b-c1ff32a217bb
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03c5ffd7-107a-437b-a90d-769d6eef4970
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x$mem_tmp == 0 || x$mem_tmp == 1) || x$mem_tmp ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2613f58-8545-4cd9-b8e3-ea8366fe14d4
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x$mem_tmp == 0 || x$mem_tmp == 1) || x$mem_tmp ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06123425-008a-4e4d-8ab9-41fd4b8916dd
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x$mem_tmp == 0 || x$mem_tmp == 1) || x$mem_tmp ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1934ff7-547f-4cee-bce6-61f474965b5e
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb20aef5-4be6-47c9-b82b-99f921571677
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4df70683-afcb-4bf6-9646-06e4d38b4fe8
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0e02dd3-9450-4e36-aedd-6b6e40f7e0f5
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 66530e85-0dd0-4011-a644-1d1f657ce8a9
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b00c47f-d8aa-4e42-8205-db74283c9fdc
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d7f1c04-4224-4be9-bcda-ebf503e7eec5
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0927bf5-b898-42d6-a857-a7c55e3b09dd
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 263c901b-0881-48f2-85bc-4190b5f54344
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a4a76e6-6573-4c98-9778-3bc1436a8514
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2072c98-5398-4ccd-bbc6-110990a63b42
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c73d671c-5543-446f-8bbf-0c307a71c686
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 88fd971b-cb02-4fd9-936d-bdcbfc42017b
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45bd9e3e-4247-49f2-98ff-9ec02b330c47
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1bdb102-d1e0-4a3c-96e5-ec6cfd388bab
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b497ada7-5746-43e8-92a9-90aeddb7c0ed
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    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: ad14d26a-e0d6-4ddb-9f58-733eef4d9f6c
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    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: 61c16fd0-7f8b-4613-9130-2f58c3f31640
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    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: 7c19417c-b630-4cdd-b722-aa9eccf8d6d9
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29b70754-c51f-4e2e-aeff-8874b5940770
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1791e8b1-2325-4295-9249-1c1a29570912
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 88b3194a-eb45-4377-ae1e-58f93937d61f
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 822be9c3-6915-4dd4-b89f-e307d3e40676
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 336a287d-8c72-4da0-baed-48e42c726e3e
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5dfda7a6-5b88-447a-94b6-cf9f4edda213
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1977848-88e8-458b-85aa-0ca9fcc1fa60
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b60780d5-e82e-4692-b4cd-b54f27d4f116
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa261904-94f0-481e-b244-b9b40da696a6
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54e17a45-ab74-40de-be99-442e63d71913
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f8f5495-2059-4a43-85af-1c37ba41ae06
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9af572a0-c2c7-4cdf-835a-11e46b64a0be
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0a45351-bb9d-41e4-98d1-049cd363c20e
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f149cf9-f2c5-4735-b407-878a07ed2d47
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f42c27f-902e-46cc-a133-d42a179ec883
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c210f0cf-6ded-4c02-9a99-bdc4c6b6a5a1
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7310961b-ebdc-4305-8fd7-28c4fdf9e7cd
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 549eb1e4-7d5b-4429-816d-d48657d3dacc
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54c62f96-8d82-4dd9-8688-5336f9d88fea
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7835229f-a88c-4d00-8a37-7fe3142d1fae
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80285ae4-ed36-4f40-a42a-73fc96ab332a
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 30130e4a-3149-4010-a21d-0a3253ff75cd
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a97b531-d35d-4cf9-a645-eef2428d69bc
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c27200ad-594f-40cc-9c4f-60ba40386366
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5fe18246-b9f5-46c5-b294-096a90406140
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f2dffe4-c550-4d7b-9fdc-602f4e1da798
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dfbea441-9647-49f3-b986-f405f129b938
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 973a223a-feea-4b4c-8f08-72d41a043021
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b86ba110-1511-445a-ae40-328f9dc1c10f
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc82d94a-0083-4787-86e2-a20b4939592b
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c69bfee0-890f-4e4b-b1f0-74bca9366a3e
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef68120a-1b36-4e36-81f0-c36e730c5578
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cbabf429-f0ed-4542-9bb3-5119daf379be
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6cfa3be-0d80-4724-b244-d92e4bff43d7
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0794ac65-c5f0-41d2-9064-710e816afb03
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20f1f611-3ccf-4226-9995-8cfc72e37c89
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 695874b0-614f-4354-9d66-70703e926342
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47fd994c-ff59-46f9-b8a1-2a47e1ed1fac
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: efb2cb0a-aadf-4574-95f8-5f08ce5556fb
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x$w_buff1 == 0 || x$w_buff1 == 1) || x$w_buff1 ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 192abb00-e5b4-440b-b54e-b2b0e19af55a
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x$w_buff1 == 0 || x$w_buff1 == 1) || x$w_buff1 ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4598760-942f-4de9-b8a7-93e5adaa55ac
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((x$w_buff1 == 0 || x$w_buff1 == 1) || x$w_buff1 ==
      2)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c79f9c1f-7b06-4c64-b42c-44d73ec370b1
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    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: 6df2037e-73aa-4ae6-b551-13c5d97cc5b6
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    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: 42ee1172-ed87-499b-91b2-ab017c1eb39f
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    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: 157c9eac-c04b-4347-a8ee-b8aa435f63a5
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b8f4c96-efab-4eda-8549-2616cf1c98e5
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b4c6a04-9656-4f8a-8629-bce71a775937
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: bc045470-01ec-4f79-a9e1-76d76ad64481
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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: b6ae72c4-f15d-4463-9215-d5393301dd85
    creation_time: 2024-07-04T11:58:20Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--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/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      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/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 874
    column: 3
    function: main
