- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5bfb663-d75f-45ad-8130-fb2b86151f4f
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c76ba2d8-81d3-425c-9d79-59a4cd3adfa4
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4195165-4b34-4def-ad02-95fcb3ceb3ba
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec44049d-43cb-45b0-baf2-2ffbc0e75b76
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 760a6a8f-0386-4591-b02c-0d94a85b9bf5
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 228e91ef-837f-42bf-a1a7-5ebd952a5c12
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EAX && __unbuffered_p0_EAX
      <= 1) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d96cbc5e-6b53-4338-9493-c775463ad796
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 1) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 725dc025-36fb-4dd0-9f03-8ac860607e46
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 1) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07a2f3a4-c7f5-4d10-a198-e013eba2825e
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 1) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c65e4d9-200c-4982-9b1a-8df92a77b7ad
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    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: af97dc19-3ea3-46f1-8503-bf9776d05c45
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    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: 6fb57c8b-65f1-4f9c-a4b4-7afb2d74d9e4
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    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: 387ee1aa-ee8f-48b0-a0e4-acda60023beb
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    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: 8fb0dbdd-a8f4-4a1e-bb39-90c4b7587b1b
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    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: 7c8bca8e-e5be-4051-88ba-250d59c85d61
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    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: ea688201-696a-4662-994d-1908c3e88020
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p1_EAX)
      && 0 <= __unbuffered_p1_EBX) && 0 <= __unbuffered_p2_EAX) && 0 <= __unbuffered_p2_EBX)
      && 0 <= a) && 0 <= b) && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) &&
      0 <= z$w_buff0) && 0 <= z$w_buff1) && __unbuffered_p0_EAX <= 1) && __unbuffered_p1_EAX
      <= 1) && __unbuffered_p1_EBX <= 1) && __unbuffered_p2_EAX <= 1) && __unbuffered_p2_EBX
      <= 1) && a <= 1) && b <= 1) && x <= 1) && y <= 1) && z <= 1) && z$mem_tmp <=
      1) && z$w_buff0 <= 1) && z$w_buff1 <= 1) && 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_buff1_thd0 == (_Bool)0) && z$r_buff1_thd1 == (_Bool)0) &&
      z$r_buff1_thd2 == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var
      == 0) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1)) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p2_EBX
      == 0 || __unbuffered_p2_EBX == 1)) && (a == 0 || a == 1)) && (b == 0 || b ==
      1)) && (x == 0 || x == 1)) && (y == 0 || y == 1)) && (z == 0 || z == 1)) &&
      (z$mem_tmp == 0 || z$mem_tmp == 1)) && (z$w_buff0 == 0 || z$w_buff0 == 1)) &&
      (z$w_buff1 == 0 || z$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e63b37ad-1b5c-41c8-98e5-01aa99e9dc88
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p1_EAX)
      && 0 <= __unbuffered_p1_EBX) && 0 <= __unbuffered_p2_EAX) && 0 <= __unbuffered_p2_EBX)
      && 0 <= a) && 0 <= b) && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) &&
      0 <= z$w_buff0) && 0 <= z$w_buff1) && __unbuffered_p0_EAX <= 1) && __unbuffered_p1_EAX
      <= 1) && __unbuffered_p1_EBX <= 1) && __unbuffered_p2_EAX <= 1) && __unbuffered_p2_EBX
      <= 1) && a <= 1) && b <= 1) && x <= 1) && y <= 1) && z <= 1) && z$mem_tmp <=
      1) && z$w_buff0 <= 1) && z$w_buff1 <= 1) && 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_buff1_thd0 == (_Bool)0) && z$r_buff1_thd1 == (_Bool)0) &&
      z$r_buff1_thd2 == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var
      == 0) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1)) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p2_EBX
      == 0 || __unbuffered_p2_EBX == 1)) && (a == 0 || a == 1)) && (b == 0 || b ==
      1)) && (x == 0 || x == 1)) && (y == 0 || y == 1)) && (z == 0 || z == 1)) &&
      (z$mem_tmp == 0 || z$mem_tmp == 1)) && (z$w_buff0 == 0 || z$w_buff0 == 1)) &&
      (z$w_buff1 == 0 || z$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37b2cdce-20d0-40bd-84f8-b801fbb4c4c4
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p1_EAX)
      && 0 <= __unbuffered_p1_EBX) && 0 <= __unbuffered_p2_EAX) && 0 <= __unbuffered_p2_EBX)
      && 0 <= a) && 0 <= b) && 0 <= x) && 0 <= y) && 0 <= z) && 0 <= z$mem_tmp) &&
      0 <= z$w_buff0) && 0 <= z$w_buff1) && __unbuffered_p0_EAX <= 1) && __unbuffered_p1_EAX
      <= 1) && __unbuffered_p1_EBX <= 1) && __unbuffered_p2_EAX <= 1) && __unbuffered_p2_EBX
      <= 1) && a <= 1) && b <= 1) && x <= 1) && y <= 1) && z <= 1) && z$mem_tmp <=
      1) && z$w_buff0 <= 1) && z$w_buff1 <= 1) && 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_buff1_thd0 == (_Bool)0) && z$r_buff1_thd1 == (_Bool)0) &&
      z$r_buff1_thd2 == (_Bool)0) && z$read_delayed == (_Bool)0) && z$read_delayed_var
      == 0) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX == 1)) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1)) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1)) && (__unbuffered_p2_EBX
      == 0 || __unbuffered_p2_EBX == 1)) && (a == 0 || a == 1)) && (b == 0 || b ==
      1)) && (x == 0 || x == 1)) && (y == 0 || y == 1)) && (z == 0 || z == 1)) &&
      (z$mem_tmp == 0 || z$mem_tmp == 1)) && (z$w_buff0 == 0 || z$w_buff0 == 1)) &&
      (z$w_buff1 == 0 || z$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d42355b-b4dc-4689-b8f2-1981450d3ea7
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 558d2831-78d1-43dd-8c40-d52424335516
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef808d49-acd6-421d-8c00-4c33e59cc106
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15f987ec-a625-4af4-ac6c-29fdc3e95a08
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    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: f1d5b982-a128-413b-b5d0-d6bb13767b7e
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    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: 0807f1dd-a05d-4b6e-a105-7d8859bb32e6
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    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: 4975da15-eb29-495e-b2ed-6c65aa72e260
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff0 && z$w_buff0 <= 1) && (z$w_buff0
      == 0 || z$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae3293eb-72e7-4f86-ab32-f7f7999d7f85
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff0 && z$w_buff0 <= 1) && (z$w_buff0
      == 0 || z$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 507ff301-eaf7-4bb7-9bf9-ef25c334cb05
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff0 && z$w_buff0 <= 1) && (z$w_buff0
      == 0 || z$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b742a5ba-14e4-4db0-b28c-27a10613d74c
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80bac7bf-f689-4e41-959a-e13ecb8b7dd8
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bdc09348-bbcd-4b72-b393-77f94a8abd00
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84731269-edab-46f0-952b-ff9511a0c3c0
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    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: cfe143f6-de69-4406-8c73-33b21794d2a0
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    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: 8a7e6631-2619-45e3-9856-219bbdd979cb
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    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: b2db9341-e4cd-47db-83e4-ba5fa09d1585
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 1) && (z$mem_tmp
      == 0 || z$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e953ea40-5b25-4c3d-90fc-06dcf39c7cb1
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 1) && (z$mem_tmp
      == 0 || z$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d54d4fce-abbd-468f-9ea8-3ae33deadfab
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$mem_tmp && z$mem_tmp <= 1) && (z$mem_tmp
      == 0 || z$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73331778-e6f9-47fc-b21f-a3dac59cfa96
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b && b <= 1) && (b == 0 || b == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1040d7e3-cb3b-4ab0-90d8-592936688e1d
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b && b <= 1) && (b == 0 || b == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ee3b046-934a-4fda-87b2-409f5d34630a
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= b && b <= 1) && (b == 0 || b == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f985f65a-d21d-4b8c-bd7e-affeaf46c678
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    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: b8450546-0fb8-4fab-afee-9c2047917ef4
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    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: 0c25883f-3bfb-4ec8-9cd7-bc28badabffe
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    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: a78d845f-1281-4478-b459-2da33737a466
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    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: 8c15e54b-66f0-4fd2-9222-5d4c96339501
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    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: 4af901e0-c77e-4f20-8378-052c53deb7e2
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    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: 535ebd57-e11b-488f-9bce-244e724c7361
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fc66185-f1c2-4ec6-bdb7-f2992c87e0f2
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9273877-0b82-4324-915b-9e9a9d592551
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc3ea5a5-59c0-4617-b4eb-da9d8f952555
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    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: 314a59e5-a82f-4f24-9719-31688091b1a0
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    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: 81878da9-cb1f-4172-ad46-2e01284cfacb
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    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: 6b28ab9c-6d75-4113-97d0-b8b115b6b166
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff1 && z$w_buff1 <= 1) && (z$w_buff1
      == 0 || z$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 848644cf-015d-474b-bbc9-7ff971cd4b2b
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff1 && z$w_buff1 <= 1) && (z$w_buff1
      == 0 || z$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81805636-3ab9-4fd9-9764-afd192d53f04
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= z$w_buff1 && z$w_buff1 <= 1) && (z$w_buff1
      == 0 || z$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8663e18-a595-4680-997c-1d5a810e3491
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 764ea728-12d8-4906-8221-35606c0f0963
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04ffc3c4-68a9-482b-9c9a-44c5b87a7c89
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 859252f5-196e-4474-9f25-68affc3f9208
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    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: ad8ea5ea-91c6-40fb-985c-fbd866d91fc3
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    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: 126afa27-da16-4743-8425-9474f4440fe8
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    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: 734e5bb2-0f6e-4547-bdbe-c6fafcae0122
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd18ba1f-1ac7-4d8c-a758-060749814238
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 728be290-6c39-40dc-b038-62ccaffa701f
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe0f4d51-94af-414b-9fe3-ed5797350728
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    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: 1b89dede-c85e-40bc-88f6-75c1efd0ff6a
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    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: da29651d-0f90-44b3-b056-3493a6a2b185
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    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: 6f3622a7-6033-45b9-8730-a3c32ad6fa5f
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 848
    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: 1421d995-8163-4b44-8ab4-0b6211817cd2
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 850
    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: caca5259-a550-4d0b-af92-a19a35a24cb8
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 2dae8df0-a113-4148-baf1-aa174ac7585a
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      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: 13928f47-63f5-4b1f-b4ee-f222ebbaded7
    creation_time: 2024-06-18T14:55:16Z
    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/mix032.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix032.opt.i: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
      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/mix032.opt.i
    file_hash: 0032fd1b0879d5a3b3f4ef67d0327f489d9a349f94447e8a77b1324c1477f2bb
    line: 846
    column: 3
    function: main
