- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70322d4c-2139-4841-8698-f2b6089bcd77
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca02afe9-d4c1-4014-bb30-c0a36c39ce16
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3477c1c5-91f8-42c5-8001-38949275c2ba
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cbed4dc-e68e-4d43-bf57-ac84b1b37870
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd4f9e57-5cb6-4b45-92de-a296abfed94e
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77b9327f-60ec-4950-81eb-be06c604b870
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a9aba9a-06d8-44ea-9976-11b97a019ac6
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c76e9ac6-0355-4e69-b7e3-4c571937c870
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3300d455-0c9d-42ae-ad7b-214f7d358919
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p3_EAX) && 0 <= __unbuffered_p3_EBX) && 0 <= a) && 0 <=
      x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0 <= z$w_buff0) && 0 <= z$w_buff1)
      && __unbuffered_p3_EAX <= 2) && __unbuffered_p3_EBX <= 1) && a <= 1) && x <=
      2) && y <= 2) && z <= 2) && z$mem_tmp <= 2) && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff1 <= 2) && z$w_buff1 <= 127) && z$flush_delayed == (_Bool)0)
      && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd1 == (_Bool)0) && z$r_buff0_thd2
      == (_Bool)0) && z$r_buff0_thd3 == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) &&
      z$r_buff1_thd1 == (_Bool)0) && z$r_buff1_thd2 == (_Bool)0) && z$r_buff1_thd3
      == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var == 0) && z$w_buff0
      % 2 == 0) && z$w_buff1 % 2 == 0) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX
      == 1)) && (a == 0 || a == 1)) && (z$w_buff0 == 0 || z$w_buff0 == 2)) && (z$w_buff1
      == 0 || z$w_buff1 == 2)) && ((__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX
      == 1) || __unbuffered_p3_EAX == 2)) && ((x == 0 || x == 1) || x == 2)) && ((y
      == 0 || y == 1) || y == 2)) && ((z == 0 || z == 1) || z == 2)) && ((z$mem_tmp
      == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bc28e4c-7cc3-4659-8313-f5b3607b9d2c
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p3_EAX) && 0 <= __unbuffered_p3_EBX) && 0 <= a) && 0 <=
      x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0 <= z$w_buff0) && 0 <= z$w_buff1)
      && __unbuffered_p3_EAX <= 2) && __unbuffered_p3_EBX <= 1) && a <= 1) && x <=
      2) && y <= 2) && z <= 2) && z$mem_tmp <= 2) && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff1 <= 2) && z$w_buff1 <= 127) && z$flush_delayed == (_Bool)0)
      && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd1 == (_Bool)0) && z$r_buff0_thd2
      == (_Bool)0) && z$r_buff0_thd3 == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) &&
      z$r_buff1_thd1 == (_Bool)0) && z$r_buff1_thd2 == (_Bool)0) && z$r_buff1_thd3
      == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var == 0) && z$w_buff0
      % 2 == 0) && z$w_buff1 % 2 == 0) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX
      == 1)) && (a == 0 || a == 1)) && (z$w_buff0 == 0 || z$w_buff0 == 2)) && (z$w_buff1
      == 0 || z$w_buff1 == 2)) && ((__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX
      == 1) || __unbuffered_p3_EAX == 2)) && ((x == 0 || x == 1) || x == 2)) && ((y
      == 0 || y == 1) || y == 2)) && ((z == 0 || z == 1) || z == 2)) && ((z$mem_tmp
      == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 487828d6-e756-463c-8391-c140cec10e8f
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p3_EAX) && 0 <= __unbuffered_p3_EBX) && 0 <= a) && 0 <=
      x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0 <= z$w_buff0) && 0 <= z$w_buff1)
      && __unbuffered_p3_EAX <= 2) && __unbuffered_p3_EBX <= 1) && a <= 1) && x <=
      2) && y <= 2) && z <= 2) && z$mem_tmp <= 2) && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff1 <= 2) && z$w_buff1 <= 127) && z$flush_delayed == (_Bool)0)
      && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd1 == (_Bool)0) && z$r_buff0_thd2
      == (_Bool)0) && z$r_buff0_thd3 == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) &&
      z$r_buff1_thd1 == (_Bool)0) && z$r_buff1_thd2 == (_Bool)0) && z$r_buff1_thd3
      == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var == 0) && z$w_buff0
      % 2 == 0) && z$w_buff1 % 2 == 0) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX
      == 1)) && (a == 0 || a == 1)) && (z$w_buff0 == 0 || z$w_buff0 == 2)) && (z$w_buff1
      == 0 || z$w_buff1 == 2)) && ((__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX
      == 1) || __unbuffered_p3_EAX == 2)) && ((x == 0 || x == 1) || x == 2)) && ((y
      == 0 || y == 1) || y == 2)) && ((z == 0 || z == 1) || z == 2)) && ((z$mem_tmp
      == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39819fb7-da6b-47c1-a0f8-defaf359dd3d
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p3_EAX) && 0 <= __unbuffered_p3_EBX) && 0 <= a) && 0 <=
      x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) && 0 <= z$w_buff0) && 0 <= z$w_buff1)
      && __unbuffered_p3_EAX <= 2) && __unbuffered_p3_EBX <= 1) && a <= 1) && x <=
      2) && y <= 2) && z <= 2) && z$mem_tmp <= 2) && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff1 <= 2) && z$w_buff1 <= 127) && z$flush_delayed == (_Bool)0)
      && z$r_buff0_thd0 == (_Bool)0) && z$r_buff0_thd1 == (_Bool)0) && z$r_buff0_thd2
      == (_Bool)0) && z$r_buff0_thd3 == (_Bool)0) && z$r_buff1_thd0 == (_Bool)0) &&
      z$r_buff1_thd1 == (_Bool)0) && z$r_buff1_thd2 == (_Bool)0) && z$r_buff1_thd3
      == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var == 0) && z$w_buff0
      % 2 == 0) && z$w_buff1 % 2 == 0) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX
      == 1)) && (a == 0 || a == 1)) && (z$w_buff0 == 0 || z$w_buff0 == 2)) && (z$w_buff1
      == 0 || z$w_buff1 == 2)) && ((__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX
      == 1) || __unbuffered_p3_EAX == 2)) && ((x == 0 || x == 1) || x == 2)) && ((y
      == 0 || y == 1) || y == 2)) && ((z == 0 || z == 1) || z == 2)) && ((z$mem_tmp
      == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7873bb8b-6f7c-41a3-a036-98a4e34a9291
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 2) && ((z$mem_tmp
      == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf3dafa3-0093-448b-ae05-8d0376c229d4
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 2) && ((z$mem_tmp
      == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f32efb05-e762-4eb1-b263-49322dd5c4ed
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 2) && ((z$mem_tmp
      == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6569486d-1e45-4398-995a-66f7bef376af
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 2) && ((z$mem_tmp
      == 0 || z$mem_tmp == 1) || z$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0de69abb-d814-4c26-98d3-155557c6f93e
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 982984c1-8777-4a9d-8051-7d7973e097ba
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bcaccd49-7710-47fd-8852-c90250cf7d54
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd91090b-4a4c-455b-917c-b4d482c2948f
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5196a442-abbe-475d-b2fa-5751c4c4cf59
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d66af42-519f-49aa-b7af-06eb2828fa4d
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9308db1-c006-488c-9cd1-f30dc76f1995
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6db2891b-9900-4d74-9bbe-0f3e35c80305
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EBX && __unbuffered_p3_EBX
      <= 1) && (__unbuffered_p3_EBX == 0 || __unbuffered_p3_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3df8f66d-ad60-49e5-b57c-9d07c98b3224
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 2) && ((__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1) || __unbuffered_p3_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68836cdf-786c-40b3-97ad-957fa989a470
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 2) && ((__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1) || __unbuffered_p3_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00f9b4c5-b4e9-4dd6-9105-255ab94bcc73
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 2) && ((__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1) || __unbuffered_p3_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d43fd8c2-3ec4-466c-8124-b5ff06cdd867
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 2) && ((__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1) || __unbuffered_p3_EAX
      == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f774185-b804-4c4e-b812-84f444d49f81
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c741c7b7-299a-4914-95ec-c98e0edfa989
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf961f56-4243-42c0-9b29-15aeff5f9d58
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7eba89c1-2e2b-4623-a273-c410725a5703
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bcd6f856-4a54-4176-a464-f0c12e4d4707
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7da43f81-00df-4744-a310-b870eb24029c
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 441a809c-1042-48fe-8776-1489474cfd49
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c279ae30-ef27-43b6-bfa6-371db555ae32
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 100da696-0f8c-460e-b9f0-d820d39e6470
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a851ad51-6f73-4d9f-a734-507c2c10e6e5
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22439f7d-15bd-45c2-836e-09596bbd8d96
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b17e4a10-5d44-43d3-b012-632f558c016d
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cddd8df7-431a-46ba-8efc-0b8685f33ed1
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 2) && ((z == 0 || z == 1) || z ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1e00909-bcf1-4bfd-be18-3d6ca697aa0d
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 2) && ((z == 0 || z == 1) || z ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fed4dda-3bd1-4dc8-a982-5016623360d6
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 2) && ((z == 0 || z == 1) || z ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f47a2fe-9b01-4ab5-b2d3-6368639dd833
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 2) && ((z == 0 || z == 1) || z ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 548a4cbc-437e-46d2-9925-753c5a2e6d07
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff0 && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff0 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dfb0c331-8f8c-4a0d-9ad4-585e5aaf239f
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff0 && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff0 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cfe68aee-ccb5-4aa0-b5ea-51beb1613cb8
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff0 && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff0 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 59de2b56-f095-401b-b5ac-ca2aecdbda16
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff0 && z$w_buff0 <= 2) && z$w_buff0
      <= 127) && z$w_buff0 % 2 == 0) && (z$w_buff0 == 0 || z$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e5ffb76-5cc1-4e66-9570-2131af600b48
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff1 && z$w_buff1 <= 2) && z$w_buff1
      <= 127) && z$w_buff1 % 2 == 0) && (z$w_buff1 == 0 || z$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95190576-5c5f-4ac1-bd0a-0b0c3f21f8f9
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff1 && z$w_buff1 <= 2) && z$w_buff1
      <= 127) && z$w_buff1 % 2 == 0) && (z$w_buff1 == 0 || z$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78b2636d-e790-4187-9656-e1107b0155c7
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff1 && z$w_buff1 <= 2) && z$w_buff1
      <= 127) && z$w_buff1 % 2 == 0) && (z$w_buff1 == 0 || z$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3be511cb-f4dd-4dee-a88b-989c594c7e2b
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= z$w_buff1 && z$w_buff1 <= 2) && z$w_buff1
      <= 127) && z$w_buff1 % 2 == 0) && (z$w_buff1 == 0 || z$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f77f80e3-a27c-46d0-a8e5-f21491e961bf
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53a50525-1afd-4232-9973-e61e0efe8ec2
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e75de341-fbfc-4522-9130-25dad3bef9e2
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ed28c44-5d83-4e54-9382-d4f864397446
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4aaa4b4-41f0-4d6d-bbbb-e9cbb090481a
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fae9536-b2c7-4d85-93df-2fac3dfada11
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1096145-7016-42e4-bc4e-47f6d1ceeda7
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc1eabcc-01c7-4591-988a-1e6a22472056
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17dc4652-ba42-4520-8306-08266f46bbcd
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7295dddb-b91d-42d0-b5b3-6462fdd5492c
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a62bb789-9f82-49ae-86cd-88f8143632dc
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f9af8ff-5012-49fa-a697-ba8b701914fd
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32b709f5-235e-4a83-abe3-fcf25c459594
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf050eff-19a8-45f6-8631-ec6d5edd4d05
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e28cb62-39ca-48af-993c-17126b419fb5
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8478442c-d7cd-454b-be75-079e64f5b417
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5fdad9ce-dd7e-4c15-8c7f-b2660b83b826
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04e6267b-0a0f-48f9-959f-59f069898618
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c71b5508-b9d0-4092-a2ae-7cff05442bb3
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af70571f-c050-4c20-a820-b02ca132282c
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b69a9e48-e2e8-452c-aeed-2e193aed5997
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50e1a219-18c7-46d9-9ca4-56388a3dca40
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    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: d9b14652-2bec-47b7-9375-39acefcb7008
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    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: efdd43f4-0985-4f11-94ee-0bf5fc9e77fe
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    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: 5a1e52b4-35fd-41fd-87ea-bc110d5a5c0b
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92db4e2d-aa21-47c2-95fc-67398bf1ad56
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2a4c1dc-716c-4f9c-9357-f0ca5124cf51
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1715f28-bf21-482c-a397-794ab0d9efb0
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d026e248-bc55-4345-9dcb-459bdfc24008
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 855
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 392482f7-9614-4a77-b2b8-0104f44f18b0
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 857
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 276ff15b-dea2-48e8-aa55-ad358cef4c39
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 859
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16a6a3d4-bd37-4a68-a597-50cf36557922
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 860
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: f237c1c4-bc88-4bb3-8b16-c3c8e12d9f92
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      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: a30382f2-9c4b-4ae6-ab34-5bda8645b0b8
    creation_time: 2024-06-18T14:55:14Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix030_tso.i: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
      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/mix030_tso.i
    file_hash: 20a2c57970e5e291ffc10826c9a5fbe3296a1e55ae86cfd2b786718aae571bfa
    line: 853
    column: 3
    function: main
