- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e9c76ff-3966-489d-b421-28705531b0c5
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$w_buff0 && x$w_buff0 <= 2) && ((x$w_buff0
      == 0 || x$w_buff0 == 1) || x$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fc3b2b5-3647-4a01-a90a-70c9ab7a37ce
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$w_buff0 && x$w_buff0 <= 2) && ((x$w_buff0
      == 0 || x$w_buff0 == 1) || x$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e75b8f09-9f47-48c4-a28d-71ea968c099e
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$w_buff0 && x$w_buff0 <= 2) && ((x$w_buff0
      == 0 || x$w_buff0 == 1) || x$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b8427ee-63e3-49a8-a6bb-8b66a32f4240
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p2_EAX)
      && 0 <= __unbuffered_p2_EBX) && 0 <= x) && 0 <= x$mem_tmp) && 0 <= x$w_buff0)
      && 0 <= x$w_buff1) && 0 <= y) && __unbuffered_p0_EAX <= 2) && __unbuffered_p2_EAX
      <= 0) && __unbuffered_p2_EAX <= 2) && __unbuffered_p2_EBX <= 0) && __unbuffered_p2_EBX
      <= 1) && x <= 2) && x$mem_tmp <= 2) && x$w_buff0 <= 2) && x$w_buff1 <= 2) &&
      y <= 1) && __unbuffered_p2_EAX$flush_delayed == (_Bool)0) && __unbuffered_p2_EAX$mem_tmp
      == 0) && __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff0 == 0) && __unbuffered_p2_EAX$w_buff0_used
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff1 == 0) && __unbuffered_p2_EAX$w_buff1_used
      == (_Bool)0) && x$flush_delayed == (_Bool)0) && x$r_buff0_thd0 == (_Bool)0)
      && x$r_buff0_thd1 == (_Bool)0) && x$r_buff0_thd3 == (_Bool)0) && x$r_buff1_thd0
      == (_Bool)0) && x$r_buff1_thd1 == (_Bool)0) && x$r_buff1_thd3 == (_Bool)0) &&
      x$read_delayed == (_Bool)0) && x$read_delayed_var == 0) && (__unbuffered_p2_EAX$read_delayed_var
      == 0 || (__unbuffered_p2_EAX$read_delayed_var == & x && ((0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 2) && ((*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1) || *__unbuffered_p2_EAX$read_delayed_var
      == 2))))) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1)) && (y ==
      0 || y == 1)) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) ||
      __unbuffered_p0_EAX == 2)) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)) && ((x == 0 || x == 1) || x == 2)) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)) && ((x$w_buff0 == 0 || x$w_buff0
      == 1) || x$w_buff0 == 2)) && ((x$w_buff1 == 0 || x$w_buff1 == 1) || x$w_buff1
      == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 915bf454-8b24-4c86-8a16-3d1c16e108ea
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p2_EAX)
      && 0 <= __unbuffered_p2_EBX) && 0 <= x) && 0 <= x$mem_tmp) && 0 <= x$w_buff0)
      && 0 <= x$w_buff1) && 0 <= y) && __unbuffered_p0_EAX <= 2) && __unbuffered_p2_EAX
      <= 0) && __unbuffered_p2_EAX <= 2) && __unbuffered_p2_EBX <= 0) && __unbuffered_p2_EBX
      <= 1) && x <= 2) && x$mem_tmp <= 2) && x$w_buff0 <= 2) && x$w_buff1 <= 2) &&
      y <= 1) && __unbuffered_p2_EAX$flush_delayed == (_Bool)0) && __unbuffered_p2_EAX$mem_tmp
      == 0) && __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff0 == 0) && __unbuffered_p2_EAX$w_buff0_used
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff1 == 0) && __unbuffered_p2_EAX$w_buff1_used
      == (_Bool)0) && x$flush_delayed == (_Bool)0) && x$r_buff0_thd0 == (_Bool)0)
      && x$r_buff0_thd1 == (_Bool)0) && x$r_buff0_thd3 == (_Bool)0) && x$r_buff1_thd0
      == (_Bool)0) && x$r_buff1_thd1 == (_Bool)0) && x$r_buff1_thd3 == (_Bool)0) &&
      x$read_delayed == (_Bool)0) && x$read_delayed_var == 0) && (__unbuffered_p2_EAX$read_delayed_var
      == 0 || (__unbuffered_p2_EAX$read_delayed_var == & x && ((0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 2) && ((*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1) || *__unbuffered_p2_EAX$read_delayed_var
      == 2))))) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1)) && (y ==
      0 || y == 1)) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) ||
      __unbuffered_p0_EAX == 2)) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)) && ((x == 0 || x == 1) || x == 2)) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)) && ((x$w_buff0 == 0 || x$w_buff0
      == 1) || x$w_buff0 == 2)) && ((x$w_buff1 == 0 || x$w_buff1 == 1) || x$w_buff1
      == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6a06f02-d39b-415c-8c35-614cdaab8652
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || ((((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p2_EAX)
      && 0 <= __unbuffered_p2_EBX) && 0 <= x) && 0 <= x$mem_tmp) && 0 <= x$w_buff0)
      && 0 <= x$w_buff1) && 0 <= y) && __unbuffered_p0_EAX <= 2) && __unbuffered_p2_EAX
      <= 0) && __unbuffered_p2_EAX <= 2) && __unbuffered_p2_EBX <= 0) && __unbuffered_p2_EBX
      <= 1) && x <= 2) && x$mem_tmp <= 2) && x$w_buff0 <= 2) && x$w_buff1 <= 2) &&
      y <= 1) && __unbuffered_p2_EAX$flush_delayed == (_Bool)0) && __unbuffered_p2_EAX$mem_tmp
      == 0) && __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff0_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd1
      == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0) && __unbuffered_p2_EAX$r_buff1_thd3
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff0 == 0) && __unbuffered_p2_EAX$w_buff0_used
      == (_Bool)0) && __unbuffered_p2_EAX$w_buff1 == 0) && __unbuffered_p2_EAX$w_buff1_used
      == (_Bool)0) && x$flush_delayed == (_Bool)0) && x$r_buff0_thd0 == (_Bool)0)
      && x$r_buff0_thd1 == (_Bool)0) && x$r_buff0_thd3 == (_Bool)0) && x$r_buff1_thd0
      == (_Bool)0) && x$r_buff1_thd1 == (_Bool)0) && x$r_buff1_thd3 == (_Bool)0) &&
      x$read_delayed == (_Bool)0) && x$read_delayed_var == 0) && (__unbuffered_p2_EAX$read_delayed_var
      == 0 || (__unbuffered_p2_EAX$read_delayed_var == & x && ((0 <= *__unbuffered_p2_EAX$read_delayed_var
      && *__unbuffered_p2_EAX$read_delayed_var <= 2) && ((*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1) || *__unbuffered_p2_EAX$read_delayed_var
      == 2))))) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1)) && (y ==
      0 || y == 1)) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) ||
      __unbuffered_p0_EAX == 2)) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX
      == 1) || __unbuffered_p2_EAX == 2)) && ((x == 0 || x == 1) || x == 2)) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)) && ((x$w_buff0 == 0 || x$w_buff0
      == 1) || x$w_buff0 == 2)) && ((x$w_buff1 == 0 || x$w_buff1 == 1) || x$w_buff1
      == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1baeef78-d404-4fa2-8bcf-4ce4c98d8321
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 030efffd-870b-4f7c-99ee-0200fea18c95
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2c44e43-f333-4887-8499-3605d78e0e77
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebdf5561-8c47-4f01-be9d-118a9d096ece
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82595339-9185-42cc-9474-e4beec74ed20
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d860cb9-dad5-4a89-b5f4-c3d08a9209a0
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 091623c3-e436-408d-b8de-74717bc71b98
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 717dea08-ad46-49d2-9115-7d74858f0e9c
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da1931d4-2832-4cfe-aeae-bfea3c664e17
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9d22e35-6b7a-41e4-89a2-841cb3f28e87
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX$read_delayed_var == 0 || (((0
      <= *__unbuffered_p2_EAX$read_delayed_var && *__unbuffered_p2_EAX$read_delayed_var
      <= 2) && __unbuffered_p2_EAX$read_delayed_var == & x) && ((*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1) || *__unbuffered_p2_EAX$read_delayed_var
      == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 356f7c84-2cef-4693-8ec6-e6124f903e3f
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX$read_delayed_var == 0 || (((0
      <= *__unbuffered_p2_EAX$read_delayed_var && *__unbuffered_p2_EAX$read_delayed_var
      <= 2) && __unbuffered_p2_EAX$read_delayed_var == & x) && ((*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1) || *__unbuffered_p2_EAX$read_delayed_var
      == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6ce3cec-5a11-4f60-a6aa-2277be5166ac
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX$read_delayed_var == 0 || (((0
      <= *__unbuffered_p2_EAX$read_delayed_var && *__unbuffered_p2_EAX$read_delayed_var
      <= 2) && __unbuffered_p2_EAX$read_delayed_var == & x) && ((*__unbuffered_p2_EAX$read_delayed_var
      == 0 || *__unbuffered_p2_EAX$read_delayed_var == 1) || *__unbuffered_p2_EAX$read_delayed_var
      == 2)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24aee4f3-9d2e-4433-b9d3-3993dc16ff10
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe5cbab8-701e-468d-8d46-7ddaec0b7cfc
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f77bf158-a678-4ef2-bac5-43914cc9610b
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d670d5e1-63b4-44fb-96df-5e988ff915d4
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 2) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1) || __unbuffered_p2_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 030eace9-4952-4f17-8c21-b36d517923ef
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 2) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1) || __unbuffered_p2_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 495508c9-b373-4f7d-b739-86dd25ea8756
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 2) && ((__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1) || __unbuffered_p2_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d529d830-5b2b-4bcd-85b3-ab9e58c99378
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 2) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc2a02c8-85ec-44a1-b41f-de7a83e33104
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 2) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34cff82c-e76b-4338-9749-fd0c793619d4
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 2) && ((__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1) || __unbuffered_p0_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 907aef65-9dc4-4e75-b32a-9b022fefc6ce
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06a37cf6-68bd-4b5c-b5f4-7489df04e6fd
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 579d5a32-f336-4af8-a886-ad0e169dce36
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69b37790-9af6-42bb-b8a1-a899a0b71755
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 2) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7af4a33b-d17a-4ab7-af4b-30226ca7db8e
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 2) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06756327-33ad-421c-b9c7-caced8f61a4d
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 2) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36e2147e-c441-4576-abbe-77f17b14301e
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2024e7e4-56f0-455c-b3a2-431e1a5f2036
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1273f7c-f885-4801-9fa7-e27ddf76918e
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9861bd3b-3964-4e4b-b7ba-d42f258cd7a4
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39248cb7-db0f-476e-921a-78bfc4663040
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65094670-1228-4693-865d-481ef6b9a7a7
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$mem_tmp == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ff0f221-4bd2-46c4-bab8-b6f89d7ce879
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79bbbf5f-171e-4fd0-9edd-9d6cb8e0e150
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85e93942-c235-4223-a19a-2e81479a9334
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c83f3be-3238-42db-bd84-9474267c03b4
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec19a967-5739-44b7-a0a2-da42f36ec411
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 532225e1-cd87-49d3-b1d0-9f8dd95c5c14
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9cbbc1d-47e3-4b66-9aed-15c8d21533d4
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6a1bae1-b345-426d-9fbe-003dbd140a47
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cb2d7c1-229e-4f92-9a7c-0a48bfba5fec
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b45896b0-5e03-4925-944d-b07f49fba666
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72bd285f-2cd1-4ff7-8ab4-81ba9894ff9a
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e101d085-6df7-46ba-9486-3ecc6e1c8153
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1cfde19-e3da-48fc-9a24-81e1a5f6b123
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0bd78f9-63f0-4a14-a34e-74f5059bbef1
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26ca233b-e50f-4a86-9da7-3205a3866273
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f068919-b0cf-4957-a901-de6b401f5e5b
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f188b15f-8bb0-412a-b1fd-707a8ede11ad
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d46601e1-48b3-48f0-b15a-0d995954fa42
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bf592b1-8324-437b-b7a1-db1ee295eeec
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28d6078e-e016-4b98-94e0-fa670d2f42f2
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c4ab5da-2827-496a-ae32-c0ebf02db409
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d830c68f-325a-4e0b-a465-510e9a724cdb
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d5da87f-f6a8-4a0f-b512-ef006c8d04e2
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da7c92e9-49dc-4fd2-936d-34d50004477d
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf00d40f-5983-4ab6-96d1-9868a776cdd3
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cb74a5e-bb17-4116-8888-49a98381de80
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82f80391-fa84-421d-a32a-05cf72df364c
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a492c427-bc76-44c1-8f2f-cb74f32f1647
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b42655a-a65b-4167-8b51-b6a76b43edae
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40d74982-00b7-4649-a7eb-b7e44fcab7ed
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a538c5a-e1ea-44a1-bf39-7e20dfc7b199
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d1e6af2-df71-41db-9fed-d7f87877538d
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fb19202-2b5e-43aa-b65f-d629c477104e
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7fa9ae16-896d-4a3c-8ace-65d39b588fd5
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1c3b829-8c41-4135-b414-902f52baede8
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 90afbc5a-30cd-483f-add2-4fc5922eb723
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dfa475b0-0ea4-4a6c-ad69-3458bdfffc5f
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4992f5c5-18ef-47fe-a409-77a560b721c5
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e2059cc-6d09-4cc8-a35a-291c5306330b
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4390a8c9-4f0a-4878-a6da-23f739a9b74a
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e6ac306a-c46f-4283-8877-f927645aed3f
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 533c54d8-90a7-4218-986a-4b77b117732c
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0 == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee41e9d1-84e7-4c84-aafc-7b61e2aba74a
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80112754-bd53-4876-be78-c53bceeea8ae
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d6e2c29-a9c6-4305-963c-6f91f681a628
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fcf567c-1cea-48f8-bc63-9aa42cdee722
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4dfafd3c-ddfd-4193-9f96-bf500a28ca87
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfe45a08-4bf8-4f52-9ffa-db5e274b5d11
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff0_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6be15b4-5ad8-46bd-818e-5e345d338ea7
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b96aed4a-7f30-492d-ab18-7d93cbcb5ed9
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f03ea35a-be36-4794-b983-eafb75184441
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0d51d92-93c6-4e03-8194-e32fc8f4856c
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$w_buff1 && x$w_buff1 <= 2) && ((x$w_buff1
      == 0 || x$w_buff1 == 1) || x$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 405fc50e-8ba5-4950-aa47-490b48d7cb36
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$w_buff1 && x$w_buff1 <= 2) && ((x$w_buff1
      == 0 || x$w_buff1 == 1) || x$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abc9c29e-6942-4299-8a47-74b4dc871a72
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$w_buff1 && x$w_buff1 <= 2) && ((x$w_buff1
      == 0 || x$w_buff1 == 1) || x$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f322d316-7c69-4e1d-a5d3-9dfa5c4dd40b
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 2) && ((x == 0 || x == 1) || x ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 201656d9-13b4-4358-8fbb-9fca0eff33f4
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 2) && ((x == 0 || x == 1) || x ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5fa8e350-5b8d-4240-8322-d146b0c8f398
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 2) && ((x == 0 || x == 1) || x ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a3bc1d4-b21b-492e-8e2a-86609e0bfe4f
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 876
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a511e47-aabd-446b-a985-81a46e945f59
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 878
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 90f55d52-249b-405b-93f8-a0d8a4a75284
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || __unbuffered_p2_EAX$w_buff1_used == (_Bool)0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: c8dccc49-a203-4a4e-b994-e6b09e694236
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b84ad179-d48c-4661-bd97-9e4e31b81e50
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 764
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3df84e94-c666-4219-83fa-6443725d3ed5
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 814
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 527c56a1-71c7-4f61-b6f7-385855ee98b0
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 849
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8ddebdf9-a55e-44ba-aaf6-5db647674dca
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 907
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 006eaa9a-a20c-4313-ab4c-e8d468f99acb
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 857
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 98bd40a6-1e5a-4cf3-b905-ae0496a2b78b
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 781
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c15cf975-1a68-4e3a-9895-cf2be1239064
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 846
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ff5325c6-280b-4896-a294-3e2daef19a49
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 802
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f580c257-aec1-4652-957c-fdfaa8930329
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 890
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e07e2b7a-d9eb-4d93-a580-98fb224c791b
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 813
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d82d8205-9251-40c8-9adb-0c3a2b189c94
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 782
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8c4256e2-ef56-4d58-8336-e16d0b592e9c
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 823
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: bd1b2e39-d115-4359-b150-43de5826f885
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 856
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d3eba570-6afb-48a2-99c7-b622e4fc8d72
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 762
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6bfe3eb8-e35b-4263-8555-492b0668c264
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 785
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 140718c5-80cb-4c82-af6f-e8d92f94ccfc
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 790
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 77306c5e-5237-4eda-abac-222293be2678
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 883
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7f7a8b2b-832d-472a-ba1a-31289c5f6d3a
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 859
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: acd1ab7b-02c1-4257-b37a-a708bcac1359
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 889
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a4f6dffe-e5db-4642-9035-c61a98ddc387
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 847
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 78a25dbd-d935-4f7d-8e88-b48273525cfe
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 881
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 0093dc21-d3da-42c0-b0d9-762f9f9b1f9d
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 765
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 694cd91f-fca5-47f0-97d1-2c9d23ae8f1f
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 780
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b2d302af-8eda-4224-a189-2390e661d352
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 879
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 75437d31-b176-4e3c-909c-c03a95297c36
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 828
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 35aa5c34-e552-42fe-bf56-b509c4e5db76
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 850
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ef6d9506-d5f2-4883-93ea-3f4968a58941
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 801
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ccc1926a-7eef-413a-a47c-3384f864f7c8
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 783
    column: 3
    function: P0
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: dd8230f1-8fa3-456d-9441-c7b593e69e82
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 42e64606-a47e-4c53-8c98-fded4d247cf0
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 874
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 63c576be-b150-419e-8150-8a78025275a0
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 763
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ce482d38-312d-4aa1-bdee-2750dfcd8ddc
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 820
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8444a02a-c293-4062-b726-550ebffa3c43
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 760
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 425ffaa0-682b-4e7d-accf-826d6bbd6ab7
    creation_time: 2024-04-29T11:51:41Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gabe16c034-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/safe025_power.i
    file_hash: 6b4ccd44d6ad5c937026f9c7e728382cb906c06e55c568dcdbddf828dfe89bc6
    line: 821
    column: 3
    function: P1
