- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68d482bf-c974-4cf5-a3ee-ff216279d083
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX)
      && 0 <= a) && 0 <= a$mem_tmp) && 0 <= a$w_buff0) && 0 <= a$w_buff1) && 0 <=
      x) && 0 <= y) && 0 <= z) && __unbuffered_cnt <= 0) && __unbuffered_p1_EAX <=
      0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX <= 0) && __unbuffered_p3_EAX
      <= 1) && a <= 0) && a <= 1) && a$mem_tmp <= 0) && a$mem_tmp <= 1) && a$w_buff0
      <= 1) && a$w_buff1 <= 1) && x <= 0) && x <= 2) && y <= 0) && y <= 1) && z <=
      0) && z <= 2) && a$flush_delayed == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0)
      && a$r_buff0_thd2 == (_Bool)0) && a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4
      == (_Bool)0) && a$r_buff1_thd0 == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) &&
      a$r_buff1_thd3 == (_Bool)0) && a$r_buff1_thd4 == (_Bool)0) && a$read_delayed
      == (_Bool)0) && a$read_delayed_var == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (a == 0
      || a == 1)) && (a$mem_tmp == 0 || a$mem_tmp == 1)) && (a$w_buff0 == 0 || a$w_buff0
      == 1)) && (a$w_buff1 == 0 || a$w_buff1 == 1)) && (y == 0 || y == 1)) && ((x
      == 0 || x == 1) || x == 2)) && ((z == 0 || z == 1) || z == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fcd0532c-fe63-46d8-be53-84c45e388fd2
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX)
      && 0 <= a) && 0 <= a$mem_tmp) && 0 <= a$w_buff0) && 0 <= a$w_buff1) && 0 <=
      x) && 0 <= y) && 0 <= z) && __unbuffered_cnt <= 0) && __unbuffered_p1_EAX <=
      0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX <= 0) && __unbuffered_p3_EAX
      <= 1) && a <= 0) && a <= 1) && a$mem_tmp <= 0) && a$mem_tmp <= 1) && a$w_buff0
      <= 1) && a$w_buff1 <= 1) && x <= 0) && x <= 2) && y <= 0) && y <= 1) && z <=
      0) && z <= 2) && a$flush_delayed == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0)
      && a$r_buff0_thd2 == (_Bool)0) && a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4
      == (_Bool)0) && a$r_buff1_thd0 == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) &&
      a$r_buff1_thd3 == (_Bool)0) && a$r_buff1_thd4 == (_Bool)0) && a$read_delayed
      == (_Bool)0) && a$read_delayed_var == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (a == 0
      || a == 1)) && (a$mem_tmp == 0 || a$mem_tmp == 1)) && (a$w_buff0 == 0 || a$w_buff0
      == 1)) && (a$w_buff1 == 0 || a$w_buff1 == 1)) && (y == 0 || y == 1)) && ((x
      == 0 || x == 1) || x == 2)) && ((z == 0 || z == 1) || z == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c36c972-6bf0-40c3-ab59-cd3d09ad9567
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX)
      && 0 <= a) && 0 <= a$mem_tmp) && 0 <= a$w_buff0) && 0 <= a$w_buff1) && 0 <=
      x) && 0 <= y) && 0 <= z) && __unbuffered_cnt <= 0) && __unbuffered_p1_EAX <=
      0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX <= 0) && __unbuffered_p3_EAX
      <= 1) && a <= 0) && a <= 1) && a$mem_tmp <= 0) && a$mem_tmp <= 1) && a$w_buff0
      <= 1) && a$w_buff1 <= 1) && x <= 0) && x <= 2) && y <= 0) && y <= 1) && z <=
      0) && z <= 2) && a$flush_delayed == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0)
      && a$r_buff0_thd2 == (_Bool)0) && a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4
      == (_Bool)0) && a$r_buff1_thd0 == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) &&
      a$r_buff1_thd3 == (_Bool)0) && a$r_buff1_thd4 == (_Bool)0) && a$read_delayed
      == (_Bool)0) && a$read_delayed_var == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (a == 0
      || a == 1)) && (a$mem_tmp == 0 || a$mem_tmp == 1)) && (a$w_buff0 == 0 || a$w_buff0
      == 1)) && (a$w_buff1 == 0 || a$w_buff1 == 1)) && (y == 0 || y == 1)) && ((x
      == 0 || x == 1) || x == 2)) && ((z == 0 || z == 1) || z == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9798b322-4941-4e60-9ac0-0a192be8585e
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX)
      && 0 <= a) && 0 <= a$mem_tmp) && 0 <= a$w_buff0) && 0 <= a$w_buff1) && 0 <=
      x) && 0 <= y) && 0 <= z) && __unbuffered_cnt <= 0) && __unbuffered_p1_EAX <=
      0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX <= 0) && __unbuffered_p3_EAX
      <= 1) && a <= 0) && a <= 1) && a$mem_tmp <= 0) && a$mem_tmp <= 1) && a$w_buff0
      <= 1) && a$w_buff1 <= 1) && x <= 0) && x <= 2) && y <= 0) && y <= 1) && z <=
      0) && z <= 2) && a$flush_delayed == (_Bool)0) && a$r_buff0_thd0 == (_Bool)0)
      && a$r_buff0_thd2 == (_Bool)0) && a$r_buff0_thd3 == (_Bool)0) && a$r_buff0_thd4
      == (_Bool)0) && a$r_buff1_thd0 == (_Bool)0) && a$r_buff1_thd2 == (_Bool)0) &&
      a$r_buff1_thd3 == (_Bool)0) && a$r_buff1_thd4 == (_Bool)0) && a$read_delayed
      == (_Bool)0) && a$read_delayed_var == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (a == 0
      || a == 1)) && (a$mem_tmp == 0 || a$mem_tmp == 1)) && (a$w_buff0 == 0 || a$w_buff0
      == 1)) && (a$w_buff1 == 0 || a$w_buff1 == 1)) && (y == 0 || y == 1)) && ((x
      == 0 || x == 1) || x == 2)) && ((z == 0 || z == 1) || z == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03c21c34-fbb5-4e9d-b929-b9539f14aed1
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1963cdce-fb52-4b8d-ac73-9aba7abc46d7
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76e6ff96-e330-4016-9baf-875cb80f2627
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c09f6457-e947-47ab-8083-9a074535caeb
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ffca297-1c4a-44bc-8d9a-c0689ef76d04
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$mem_tmp && a$mem_tmp <= 1) && (a$mem_tmp
      == 0 || a$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6adf618b-ebcd-4a04-9254-060739797ef8
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$mem_tmp && a$mem_tmp <= 1) && (a$mem_tmp
      == 0 || a$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6d6840d-5ea7-4d0b-9355-6c262b96c75e
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$mem_tmp && a$mem_tmp <= 1) && (a$mem_tmp
      == 0 || a$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14a686ca-2c42-40b2-bfea-52bbd51397fe
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$mem_tmp && a$mem_tmp <= 1) && (a$mem_tmp
      == 0 || a$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ba89eb5-e463-495d-8e37-b5e20dc0e48a
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 795dcd32-0b55-492d-a343-15d48c4790ac
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64845c4c-45e4-4304-8edd-54dac5a8bffc
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84c649a5-da17-420c-b415-8760f31ab60a
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e5b67b9-d2d7-44a8-aad1-41b6cf287202
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e4523b2-89b7-40e5-abdb-c9f4a262f9fc
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 739ee377-91e6-4d60-8968-fe737ceabcf9
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9863406-7a17-44ec-87a5-159de10c5391
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb8bb7fa-6f2a-4659-a599-ea0e16ce48be
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1d35297-24f1-49a7-b52f-844a401d3752
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bab00340-88a9-4566-84bd-2a66a7553ece
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9aaa7fdf-2987-4d0c-bfc1-6cdce989d52d
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 675ae5a1-a938-41b3-a0d4-fb21f5451029
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 357ec52e-cc18-4409-b257-6cc06bbe54de
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d557beaf-66cf-4f10-aa85-b1d18c05c720
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc19aa5c-a62a-4054-b4f6-3254ffacba42
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63976164-3abb-4f30-9164-734f608d4da4
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    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: a66c8b03-3c66-4a43-9792-85773d5796e3
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    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: beb4287b-d4fc-4f90-b84f-4e4ab6087586
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    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: 05b5f716-eeef-4d79-ba65-03236d3a172a
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    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: 10b22d68-7caf-446c-b596-5369c5ce10df
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6cd14e0e-a253-4ac0-8463-55d09d8879cd
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56ed7d3c-c1e8-4277-affb-27074efd268e
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bffe525f-16c4-4fa6-ab10-627e87cb8c66
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc61b8e2-8041-4a8b-822b-6962bb0c9194
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4dde78b5-1bc7-481b-a873-a153f208e68d
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd43ab6c-5858-42b6-9872-e2ae95001808
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7976a5df-0b0a-4746-8b06-c710c4e22542
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a3ae05c-29e4-4284-ba53-6ee6387f8e31
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    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: e342aa3b-d34f-4deb-9865-12f7c66af20d
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    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: 9d1b8fd4-4fa8-4946-94e6-44b898a367e5
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    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: 924611c7-5a28-422b-9eb2-1a7c387056d1
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    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: 555fd4e0-e5fe-422e-a6bc-ad7a106b1663
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62f54aa6-378e-4f3f-a607-325954c43452
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d640497a-50a4-410f-ae3a-46ffda39779f
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6793a8d2-c3eb-45c5-affe-b857211f965b
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35ecfe3e-3756-4de3-92c2-49a1d84dac26
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3829b90f-9f69-4181-9bcd-0aea471b8240
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd47f219-6bde-4223-beec-c53f8090a252
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 389d35bf-1e2f-483f-998b-fc2840b1e185
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a950e03-1499-4561-89b6-b6f600b1f4e8
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06bba527-e350-421e-baaa-307c975cbe06
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23a25ffb-4627-4e62-abe9-7043fbb9eea9
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec85fd31-0fb8-4c4c-885b-17fcdd75feaa
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa358866-7f80-4345-8972-1066408a6fd2
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c93aa9a-edd9-48d7-a658-753b6636a2df
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c195dda-58fa-4ad5-9512-52aed7d57f5c
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14d5be3e-f2fb-4c11-b4a6-9ad1827e29be
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e22fe642-41c9-4e87-8914-324c318cdc3b
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff0 && a$w_buff0 <= 1) && (a$w_buff0
      == 0 || a$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92f18cf4-f0db-416d-abfb-7d76dba7a830
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff0 && a$w_buff0 <= 1) && (a$w_buff0
      == 0 || a$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3148a69d-54b7-4399-ad0a-7d6fb2c147c6
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff0 && a$w_buff0 <= 1) && (a$w_buff0
      == 0 || a$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f67037d-a743-4bff-92a3-90c85926394f
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff0 && a$w_buff0 <= 1) && (a$w_buff0
      == 0 || a$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb9a6d92-fcad-4cdd-b502-2b50aaae53de
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bcfe5e00-1ce6-4eb5-b8db-6c57a154b42c
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24448309-3f9e-4c8a-a69c-e079f2a748dc
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb717f01-710d-4335-9a63-ecec3b08ecad
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ec481cf-3580-4561-8aad-2cc470b32192
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff1 && a$w_buff1 <= 1) && (a$w_buff1
      == 0 || a$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 88df9b46-c0fd-435c-90ba-95b07b6641b6
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff1 && a$w_buff1 <= 1) && (a$w_buff1
      == 0 || a$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d24b5f3-8c69-4d9d-91a2-48bb85a97168
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff1 && a$w_buff1 <= 1) && (a$w_buff1
      == 0 || a$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 480ee909-4028-4a83-b830-180e0df933dd
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a$w_buff1 && a$w_buff1 <= 1) && (a$w_buff1
      == 0 || a$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 491ea620-355f-4281-883a-1cf977882e23
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8724a357-c636-4190-907b-8a9d15ae4902
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6715a06e-6bc5-4bc5-b8d9-10340753e7bf
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc2cf724-dc49-4c0d-b9c3-289d6444f959
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fab48464-409b-449c-a568-d6f4439d64b2
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    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: 95acb74f-4d87-41a2-91dc-08ed22c05ee9
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    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: 104fcb59-8fb3-4c58-ad98-4b647624f825
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    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: 34e70064-5a23-43bb-9b73-6352ec3dd3a7
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    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: e8e1e2ae-d59d-43c2-9c25-5b7d557777bd
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 862
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ee45eb1-b960-4db9-9d7e-92bf48d208cd
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 864
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53685216-f5ac-4903-9c71-b3bb75cf2621
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 866
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1d068be-e116-48d4-8987-a39754912b46
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || a$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: df0d996f-1502-41f1-bd0a-3ee1adf9a778
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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: 683bc59f-52c6-4d3d-ab34-34ef7ab638ac
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 867
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7472fdb4-24fa-4c3f-a322-37b5c22f21fb
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 762
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2d70b400-601c-440c-b57a-624bfec78f7a
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 820
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 905a4e1f-1163-436b-9a78-21b689ab6438
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 789
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bd17337e-67aa-4dc1-b995-adfe9706e4e3
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 772
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: dd6c5e9c-85b6-44ef-816a-5af6275c0577
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 760
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4a2a6092-187b-4fc8-90a9-29ac02c12639
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 812
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fdd04871-cd0c-4843-9839-60b92921fef6
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 799
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5107f333-d51a-47c7-a10e-1c3262d6ce7d
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 809
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cc33aaa8-b8ef-4f69-bd55-3a2c8bc2245a
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 763
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 67a82b3f-2c90-40da-9e0a-8a9b5fa7c603
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 810
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: df567912-87f9-4db7-9871-0be212389a05
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 770
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 76e777db-e8ea-4b27-8969-b6d65429da67
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 845
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5b37d52d-d445-4ca8-9d01-3ab046cf6e00
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 843
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5984fae1-1d58-484c-a87f-21e197a7594f
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 803
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2db0e7cf-f94e-4ec1-bb33-d99fb1832e38
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 878
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3ba3c306-1159-4204-b36b-baebfe3f81f9
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 817
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4523818d-6ef7-49bc-868e-602e7a0a2af7
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 819
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3880e465-ceb3-4174-a845-8647a8e8fef0
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 880
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7483aa3c-dc08-4499-9ef9-f8066405207a
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 783
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 15386906-845e-4149-b2ae-2ecb8a2b50cf
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 842
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0474d783-d796-4668-a8f7-09caf064bf20
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 869
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 3a94e095-805f-438e-944f-1ce2572c3f69
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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: e102a2ab-156b-410c-b087-590af5d08e62
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 860
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8b815638-5a38-47e7-b04d-f2bb428f8dee
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 792
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 143c9865-5839-4a7a-b230-831c672f819c
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 836
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0ae7af1e-7818-4e3e-9627-4dbdc951b93f
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 877
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 39e17f22-b2a0-4139-8db0-e084c909630f
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 782
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bf0015b0-bcf7-40e9-8ea7-556d88af49d0
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 777
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 826f545b-d3e9-4f1d-847c-efdfb2399303
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 780
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 70aa6afa-56eb-460d-b628-71b3ae712136
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 790
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4dc3d322-71fe-4ce2-b336-50875b777e5a
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 769
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c5b09f1c-9107-4e05-946e-52cf0af2cf0d
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 835
    column: 3
    function: P3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b7dfa789-d1b2-4c43-82c4-60be8ea6c5cd
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 759
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d7a2a83b-7db5-4691-b468-412aa679b371
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 871
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3c70d88d-a5cb-4cad-9700-ad6a4b4a0788
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 747
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4638d2d5-9a9f-4eee-8428-7e9098051192
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 802
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ed5b8e68-ba4b-4047-895e-e49d29d60d55
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 797
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 75a948a1-e3fb-478d-834a-d8b9395c2b38
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 800
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1ca64050-4083-48b5-a4fd-ecb108f92b3d
    creation_time: 2024-04-29T11:49:34Z
    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/mix055_power.oepc_pso.oepc_rmo.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_power.oepc_pso.oepc_rmo.oepc.i: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
      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/mix055_power.oepc_pso.oepc_rmo.oepc.i
    file_hash: b8efebf87dc67f98045ac231dc43d6a61f436e058244f16134f1d46d3b696c80
    line: 779
    column: 3
    function: P1
