- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 507aec86-c51b-46dc-b2cb-be226f1d623f
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff1 && y$w_buff1 <= 1) && (y$w_buff1
      == 0 || y$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3bd6762-62a4-413a-8a87-c139890f468c
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff1 && y$w_buff1 <= 1) && (y$w_buff1
      == 0 || y$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45f3e9fe-2ec3-4bd1-b0e6-fa210c2816f2
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff1 && y$w_buff1 <= 1) && (y$w_buff1
      == 0 || y$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2db647b1-f176-46a2-a83e-3381c391aeff
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p1_EAX)
      && 0 <= __unbuffered_p2_EAX) && 0 <= x) && 0 <= y) && 0 <= y$mem_tmp) && 0 <=
      y$w_buff0) && 0 <= y$w_buff1) && 0 <= z) && __unbuffered_p0_EAX <= 1) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX
      <= 1) && x <= 1) && y <= 0) && y <= 1) && y$mem_tmp <= 0) && y$mem_tmp <= 1)
      && y$w_buff0 <= 0) && y$w_buff0 <= 1) && y$w_buff1 <= 0) && y$w_buff1 <= 1)
      && z <= 0) && z <= 1) && __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) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0 == (_Bool)0)
      && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd3 == (_Bool)0) && y$r_buff1_thd0
      == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) && y$r_buff1_thd3 == (_Bool)0) &&
      y$read_delayed == (_Bool)0) && y$read_delayed_var == 0) && (__unbuffered_p0_EAX
      == 0 || __unbuffered_p0_EAX == 1)) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p2_EAX$read_delayed_var
      == 0 || (__unbuffered_p2_EAX$read_delayed_var == & y && ((((0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 1) && (0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 1)) && (*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1)) && (0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 0))))) && (x == 0 || x == 1)) &&
      (y == 0 || y == 1)) && (y$mem_tmp == 0 || y$mem_tmp == 1)) && (y$w_buff0 ==
      0 || y$w_buff0 == 1)) && (y$w_buff1 == 0 || y$w_buff1 == 1)) && (z == 0 || z
      == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6a1065d-7b52-43aa-9c28-ee38a1a4eb3f
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p1_EAX)
      && 0 <= __unbuffered_p2_EAX) && 0 <= x) && 0 <= y) && 0 <= y$mem_tmp) && 0 <=
      y$w_buff0) && 0 <= y$w_buff1) && 0 <= z) && __unbuffered_p0_EAX <= 1) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX
      <= 1) && x <= 1) && y <= 0) && y <= 1) && y$mem_tmp <= 0) && y$mem_tmp <= 1)
      && y$w_buff0 <= 0) && y$w_buff0 <= 1) && y$w_buff1 <= 0) && y$w_buff1 <= 1)
      && z <= 0) && z <= 1) && __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) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0 == (_Bool)0)
      && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd3 == (_Bool)0) && y$r_buff1_thd0
      == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) && y$r_buff1_thd3 == (_Bool)0) &&
      y$read_delayed == (_Bool)0) && y$read_delayed_var == 0) && (__unbuffered_p0_EAX
      == 0 || __unbuffered_p0_EAX == 1)) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p2_EAX$read_delayed_var
      == 0 || (__unbuffered_p2_EAX$read_delayed_var == & y && ((((0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 1) && (0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 1)) && (*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1)) && (0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 0))))) && (x == 0 || x == 1)) &&
      (y == 0 || y == 1)) && (y$mem_tmp == 0 || y$mem_tmp == 1)) && (y$w_buff0 ==
      0 || y$w_buff0 == 1)) && (y$w_buff1 == 0 || y$w_buff1 == 1)) && (z == 0 || z
      == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a589c94-89d8-4784-9867-ea897ef875a0
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p1_EAX)
      && 0 <= __unbuffered_p2_EAX) && 0 <= x) && 0 <= y) && 0 <= y$mem_tmp) && 0 <=
      y$w_buff0) && 0 <= y$w_buff1) && 0 <= z) && __unbuffered_p0_EAX <= 1) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p2_EAX <= 0) && __unbuffered_p2_EAX
      <= 1) && x <= 1) && y <= 0) && y <= 1) && y$mem_tmp <= 0) && y$mem_tmp <= 1)
      && y$w_buff0 <= 0) && y$w_buff0 <= 1) && y$w_buff1 <= 0) && y$w_buff1 <= 1)
      && z <= 0) && z <= 1) && __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) && y$flush_delayed == (_Bool)0) && y$r_buff0_thd0 == (_Bool)0)
      && y$r_buff0_thd1 == (_Bool)0) && y$r_buff0_thd3 == (_Bool)0) && y$r_buff1_thd0
      == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) && y$r_buff1_thd3 == (_Bool)0) &&
      y$read_delayed == (_Bool)0) && y$read_delayed_var == 0) && (__unbuffered_p0_EAX
      == 0 || __unbuffered_p0_EAX == 1)) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p2_EAX$read_delayed_var
      == 0 || (__unbuffered_p2_EAX$read_delayed_var == & y && ((((0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 1) && (0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 1)) && (*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1)) && (0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 0))))) && (x == 0 || x == 1)) &&
      (y == 0 || y == 1)) && (y$mem_tmp == 0 || y$mem_tmp == 1)) && (y$w_buff0 ==
      0 || y$w_buff0 == 1)) && (y$w_buff1 == 0 || y$w_buff1 == 1)) && (z == 0 || z
      == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c23df3b7-26dc-4f57-a224-d22e158cbbea
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79b732f9-6f5d-4052-80bb-41eda1ddc477
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 354b899a-4e1b-49f1-b924-e194ca82f1ed
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ff71210-063c-43c0-af76-884cee0140af
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: e58b1fa4-a4a2-40b1-9056-6dea6e41404d
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 42ba06cf-1db8-4d59-8a55-97add607f5bd
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 205e7024-a097-42f6-9aad-9d89ade181a1
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12deed5c-e6f5-44c2-a156-5882c769f593
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f92dabe7-3c00-4250-a18d-4e8be8724dca
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba8fbe9b-7265-45b4-802e-2ae3172d372e
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: 9907b684-15f8-482c-a90c-8d4dd5655e0f
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 128bd7f2-e0e2-4e15-9042-8a7f6a2359c1
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 6a759301-cecd-4476-a25b-d9e84f7b6325
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: a1ecf598-2c09-4c49-8e0b-d74921db62b5
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 3b8b52fa-33e7-41be-a1b3-88ab7b50e697
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 4a56a466-3461-4254-85c9-d2a49d6b2565
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: 7ce82272-256e-4be0-936a-8fe6e2943e93
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 886dba47-2b6f-49ed-b98e-80aaef6b1b0c
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 749ff9c0-5b89-47d3-a624-26092343d0e3
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: 5153f09f-29f6-48d8-adb9-57dcf34990eb
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 1c45e0bc-fdb7-42ae-9262-11aecbb5cba9
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 7d9f42ca-6b9c-4f9e-bb40-eea79e38e9ac
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 1) && (y$mem_tmp
      == 0 || y$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26f0e879-c905-4c8f-9b67-f852d5b23da4
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 1) && (y$mem_tmp
      == 0 || y$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9085a8b-3b88-40ae-ac86-48d1defb2215
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 1) && (y$mem_tmp
      == 0 || y$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cdf88512-cc02-4c0e-8667-601d46016ad8
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: 0d6f0d43-87d7-474d-badd-7e8435a8d18b
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: d941048b-7941-4a12-88c7-8a6c007de130
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 2d928ff4-c4b0-40b3-a3d6-2b882383e331
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 761a7069-1b58-4c6a-9558-863e576462e1
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0439a94-64e3-4f4b-b660-aeb8a98babc2
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6568a160-227c-46e0-a985-5aea5aaabb31
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: 891d45ca-6cc5-44ea-89e9-e8faa83459df
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 502b19a6-ada0-430e-96ba-2fb865c368ad
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 1021b0a4-5b95-4676-ac2c-a9f8abdeafc7
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: 903a59f9-55f8-4721-88a2-a0423782606c
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 35dac8ac-0f9d-41a1-a6cb-4355a6af2482
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: c731c4bd-ef78-4fb0-90ff-fa7abb02ace6
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8673650f-9786-4ee0-ad33-5059ea65f2d9
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8971a44c-f0c9-4d48-9684-cc90ddb29897
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5c7a277-3c08-4304-acb4-1ba3830d588d
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 610bbe2b-9f3c-4049-beb6-a6c24b2cfaf9
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6d4b6a0-fc44-49a0-8a95-f78a26ee13d8
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a79f359f-9e89-4eab-a9d9-61aba82fbe9a
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff0 && y$w_buff0 <= 1) && (y$w_buff0
      == 0 || y$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2119a45-2106-4314-8451-b69d9913ca97
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff0 && y$w_buff0 <= 1) && (y$w_buff0
      == 0 || y$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05fbab38-cd39-4bac-aa1c-733830ab3aa5
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff0 && y$w_buff0 <= 1) && (y$w_buff0
      == 0 || y$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20d21bcf-1d9b-419c-abde-a85aeb9d17f0
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX$read_delayed_var == 0 || (((0
      <= *__unbuffered_p2_EAX$read_delayed_var && *__unbuffered_p2_EAX$read_delayed_var
      <= 1) && __unbuffered_p2_EAX$read_delayed_var == & y) && (*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c67ea1d-1b5b-41dd-b66a-80905c56fdcd
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX$read_delayed_var == 0 || (((0
      <= *__unbuffered_p2_EAX$read_delayed_var && *__unbuffered_p2_EAX$read_delayed_var
      <= 1) && __unbuffered_p2_EAX$read_delayed_var == & y) && (*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd2bfd88-c42f-4f58-aafc-3f0951fa450d
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX$read_delayed_var == 0 || (((0
      <= *__unbuffered_p2_EAX$read_delayed_var && *__unbuffered_p2_EAX$read_delayed_var
      <= 1) && __unbuffered_p2_EAX$read_delayed_var == & y) && (*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a44b76bf-36bc-4195-9bd2-d9fcc3c79382
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 510cbc44-0264-4988-b9a5-d2992e692e31
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b5f3b6b-37b4-4f4a-b781-5556a0808bbd
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0b09443-7158-4325-b0d4-417b2ad54ce5
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8c4d938-642f-43c2-9cb0-5279916e9b34
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab6d5245-ca86-4847-989e-91faa46fb7eb
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 441f09f8-6c7c-42d5-8687-72166cedc75b
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae7dd78e-d9f5-4ffd-831e-d7b4d57db9d3
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f03f262-7dd6-4df4-8b15-5d9a6cf36090
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b25b7c5-cbef-4509-89dc-d8a630985bf8
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: fd10d487-8909-4a85-9d60-6fd3014dc19e
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 4680dd6a-a40e-4fdd-a49c-602762599127
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 12f8cd8c-216d-408c-bc12-4f63b6db419d
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64bb9b12-b58b-45df-975a-4b45bf574893
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b84d499-744a-419f-8e51-185c4032f851
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d557d2c-89e6-4c91-927c-42716d473865
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: 0866443e-db5a-47d2-9227-9b6905df92ed
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 20bee63f-ed59-4540-952c-81fc084e00be
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 3da57293-d1c3-4588-9440-4431e8cc0e8a
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8aa0b5d0-3872-4603-b0cb-e87ec73ec14f
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fb8013a-50c4-4ea6-ab50-234e82b0a738
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da629ee7-de86-4db7-aae9-55667e8f4f0c
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97e5dc75-0a53-4d0d-ab78-bb008af4fb2c
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92e52ca4-df53-46d1-b1ff-a8b9e25c4aa6
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7079553d-5afe-4167-9d2c-0fcdff9b8a7b
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d0ef013-1500-4e68-948a-8a480b1b5e19
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0da57879-41e8-48d2-91cc-060dbe6a79e7
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c69e6817-3ef9-46c2-9006-221bef34036c
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89ca0bbc-d236-4fbf-9236-d4ed80090748
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36d2ec23-b7f0-4926-9a20-980fe875bc6c
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e646c743-b2c7-4d58-a225-e7d6f34daa4f
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db331992-5eb4-41c6-b965-23c60c3bf643
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 2b7ca706-84ff-4a1b-b32b-3e3b4b9666ca
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 14cd8c31-a9bb-4e2f-a2b6-b4d49016061c
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: 93511b30-aa5f-4885-80d2-df7b19312e27
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 72c1035b-2ceb-4f8c-a6e3-ffed1f349963
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 387b68fa-5bc7-41a5-923c-52b130022a0d
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: bdf40f58-7501-466c-b22b-bbc7238e43f4
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: bce2a737-baa0-4ad0-8b8a-21341a7358b7
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: fe949bcf-9fc3-41e7-91df-8f2e37bef2d8
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: 26ee9bba-080c-4c5b-82ca-f78cba552986
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 156ee2cf-73cb-48a4-8251-d262d74d9a6f
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    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: 5e97a6ba-d91c-4ad4-8ac1-ea82498d9e74
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5489fed8-780f-485a-b9a0-3f8f76512bee
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48c177ea-8b63-4675-9d70-559e1b384936
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea08a022-3ffb-4e54-b272-a35bf9c0615e
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 853
    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: 599ac87a-1a87-4459-b3ec-0b50ea2b1d1e
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 855
    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: 65011207-caa9-407b-bbb0-1d5682d482e4
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 5564dbb9-0ca8-442f-9c05-d8a3e578de3d
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4557e97e-439f-42ad-9303-3182bab2de2d
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 860
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7524bea6-11ac-4c7c-9109-f3d82cf9837f
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 858
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 76b58914-db2e-46d8-9b8b-9401faaad6f6
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 790
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 36ffef36-e34c-4af9-afb3-f44b1f69c8f0
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 791
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d48ec5d5-3e45-48e6-affd-b7c5f31ee44a
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 779
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 28bed229-c231-4635-93e0-0685710dde37
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 824
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c956504c-602b-4c10-b24f-40a95b08db13
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 800
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6ed2a8fe-9c59-49d9-9faa-9eadc111914d
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 776
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5116a263-9bbd-4422-946f-19025c305f45
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 778
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 74e07501-1905-4bba-8233-0a4eb4f4ba61
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 769
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b8659be0-680e-487f-b15b-0b4a99cc106a
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 871
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7333439c-c7e4-4f24-bc7c-d9a8d6b3ad05
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 771
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8f6d020b-2998-43c0-98e4-acfb33e2f898
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 798
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9a4b1aa7-c146-4039-a58b-08061468917e
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 763
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8f2793b7-648f-41e9-a62c-1c2e7c5ef92e
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 823
    column: 3
    function: P2
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 2be6a559-b5f9-440d-b2cb-48b834818f22
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      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: 95b61672-c1da-4179-826f-7229a4731f7f
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      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/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 851
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d818c60d-0eb2-47dc-a8fd-f8331f107c04
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 766
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6375a0d9-bed1-4a0b-b7e5-1be5ed5bf58f
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 866
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b656d333-f69b-433f-8ec0-51b6775e31b1
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 867
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 72f2ae0f-c06c-4fca-9a3f-630d96db68f8
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 797
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3284b8b6-2a9a-4eed-9d89-1ab2199d8210
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 856
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 64cc43f5-f37f-4d32-8791-2c455895e3e9
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 827
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7fc8a76e-3a46-4c7e-a8e3-ec1048c80834
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 805
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 92d3ad5d-93f6-47e9-acc4-4001894552e7
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 767
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cb4872b7-8c39-4435-9b1c-352b4025e06e
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 826
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7bdf5b25-df8a-4963-bbaf-f91b83cb357f
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 836
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1c76887f-31ae-4eff-9711-a736035b1207
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 764
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a9b98198-21d5-4dd7-bd4a-28cc63fa8df3
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 768
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d6addd51-caa8-48ce-b5da-89421209aeb2
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 833
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 99da04c2-b284-48ab-a84f-005408b6c2f2
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 761
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 96bc73af-4305-4139-b53a-9b0c9ff2b4a3
    creation_time: 2024-04-30T10:00:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe007_power.opt-thin001_power.opt.i
    file_hash: 6328ead9c10c029445fd051d7c6329db494c1000fb08b7313fbd69c70835e259
    line: 834
    column: 3
    function: P2
