- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82918991-e1a3-4d06-9fed-197b3cc1ee2a
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff0 && y$w_buff0 <= 1) && (y$w_buff0
      == 0 || y$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb5dd15f-aa4e-4dfb-9011-b62ae7a9d6e7
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff0 && y$w_buff0 <= 1) && (y$w_buff0
      == 0 || y$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 196ffc82-3f27-4bef-83ab-6c3851f39c23
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    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: 6bbd38fe-c9c1-4753-be97-290579403d00
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    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: 20c6678c-d8c5-41e2-bc70-80aa904e9064
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 061690a9-e238-4431-bc0c-e6886e0fd097
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b544147a-2cf8-4d5f-b0be-3aa37c73efb3
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b170a62-0fcb-4188-8f3b-a699e754a38b
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ab0e676-c738-4e43-9851-2f5a0478ee91
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    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: 42a2b63a-be5c-4f8b-944e-52b23df65f58
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    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: 3db42423-26e7-43e5-a586-5c9c195045de
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    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: 23f6219d-f733-40b2-a3cf-529848a76f99
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    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: caf535f6-ee62-4a6d-8e3e-ae9ba5e47a64
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$w_buff0_used == (_Bool)0 || y$w_buff0_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 042380b2-5631-4e50-a5bb-37bc8c991e0b
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$w_buff0_used == (_Bool)0 || y$w_buff0_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05492b2f-7aa8-48c2-ac5e-6257ca6f8e04
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2058a3de-7a7c-4b36-ab2f-dd3adfa047a2
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 666ed1e8-965d-4f52-b032-cd76f56b79b1
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$r_buff0_thd2 == (_Bool)0 || y$r_buff0_thd2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0222f87-221a-4be4-80b5-6e664cc67bfc
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$r_buff0_thd2 == (_Bool)0 || y$r_buff0_thd2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79b01b3c-0501-4185-8a2a-09fe25033b31
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$flush_delayed == (_Bool)0 || y$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c414e765-eab8-4f01-a6a8-6093bfafa31e
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$flush_delayed == (_Bool)0 || y$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 74ad3032-0788-48b0-8cc8-fa799c58b622
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    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: aeb8ef5a-7e8a-4bd5-b001-d9b9482d94bd
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    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: 7c98b0fb-6505-448b-a266-b0d47a74e38e
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    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: 3ea7eadb-1192-46f1-b960-c8795b53c9b0
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    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: 971fab2e-074d-457e-a6c0-382db7a21a31
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 447a02f7-8e8f-4b39-8c49-1b4b72d01fc4
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de76784f-28ad-4955-b436-65e5a79bc53e
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d9182a5-4f4d-4fa4-9cb0-5752f7442dfa
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82e0ea0e-bbca-4edf-941b-74f9b2765077
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p0_EBX)
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p1_EBX) && 0 <= a) && 0 <=
      x) && 0 <= y) && 0 <= y$mem_tmp) && 0 <= y$w_buff0) && 0 <= y$w_buff1) && 0
      <= z) && __unbuffered_p0_EAX <= 1) && __unbuffered_p0_EBX <= 1) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX
      <= 1) && a <= 1) && x <= 1) && y <= 1) && y$mem_tmp <= 1) && y$w_buff0 <= 1)
      && y$w_buff1 <= 1) && z <= 0) && z <= 1) && y$flush_delayed == (_Bool)0) &&
      y$r_buff0_thd0 == (_Bool)0) && y$r_buff0_thd1 == (_Bool)0) && y$r_buff1_thd0
      == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) && y$read_delayed == (_Bool)0) &&
      y$read_delayed_var == 0) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX
      == 1)) && (__unbuffered_p0_EBX == 0 || __unbuffered_p0_EBX == 1)) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1)) && (a == 0 || a == 1)) && (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0
      == (_Bool)1)) && (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 == (_Bool)1))
      && (x == 0 || x == 1)) && (y == 0 || y == 1)) && (y$mem_tmp == 0 || y$mem_tmp
      == 1)) && (y$r_buff0_thd2 == (_Bool)0 || y$r_buff0_thd2 == (_Bool)1)) && (y$r_buff1_thd2
      == (_Bool)0 || y$r_buff1_thd2 == (_Bool)1)) && (y$w_buff0 == 0 || y$w_buff0
      == 1)) && (y$w_buff0_used == (_Bool)0 || y$w_buff0_used == (_Bool)1)) && (y$w_buff1
      == 0 || y$w_buff1 == 1)) && (y$w_buff1_used == (_Bool)0 || y$w_buff1_used ==
      (_Bool)1)) && (z == 0 || z == 1)) && (weak$$choice0 == (_Bool)0 || weak$$choice0
      == (_Bool)1)) && (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d3f997a-aceb-4a5b-803c-9bdf86cba38c
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || (((((((((((((((((((((((((((((((((((((((((((((((((((0
      <= __unbuffered_cnt && 0 <= __unbuffered_p0_EAX) && 0 <= __unbuffered_p0_EBX)
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p1_EBX) && 0 <= a) && 0 <=
      x) && 0 <= y) && 0 <= y$mem_tmp) && 0 <= y$w_buff0) && 0 <= y$w_buff1) && 0
      <= z) && __unbuffered_p0_EAX <= 1) && __unbuffered_p0_EBX <= 1) && __unbuffered_p1_EAX
      <= 0) && __unbuffered_p1_EAX <= 1) && __unbuffered_p1_EBX <= 0) && __unbuffered_p1_EBX
      <= 1) && a <= 1) && x <= 1) && y <= 1) && y$mem_tmp <= 1) && y$w_buff0 <= 1)
      && y$w_buff1 <= 1) && z <= 0) && z <= 1) && y$flush_delayed == (_Bool)0) &&
      y$r_buff0_thd0 == (_Bool)0) && y$r_buff0_thd1 == (_Bool)0) && y$r_buff1_thd0
      == (_Bool)0) && y$r_buff1_thd1 == (_Bool)0) && y$read_delayed == (_Bool)0) &&
      y$read_delayed_var == 0) && (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX
      == 1)) && (__unbuffered_p0_EBX == 0 || __unbuffered_p0_EBX == 1)) && (__unbuffered_p1_EAX
      == 0 || __unbuffered_p1_EAX == 1)) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX
      == 1)) && (a == 0 || a == 1)) && (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0
      == (_Bool)1)) && (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 == (_Bool)1))
      && (x == 0 || x == 1)) && (y == 0 || y == 1)) && (y$mem_tmp == 0 || y$mem_tmp
      == 1)) && (y$r_buff0_thd2 == (_Bool)0 || y$r_buff0_thd2 == (_Bool)1)) && (y$r_buff1_thd2
      == (_Bool)0 || y$r_buff1_thd2 == (_Bool)1)) && (y$w_buff0 == 0 || y$w_buff0
      == 1)) && (y$w_buff0_used == (_Bool)0 || y$w_buff0_used == (_Bool)1)) && (y$w_buff1
      == 0 || y$w_buff1 == 1)) && (y$w_buff1_used == (_Bool)0 || y$w_buff1_used ==
      (_Bool)1)) && (z == 0 || z == 1)) && (weak$$choice0 == (_Bool)0 || weak$$choice0
      == (_Bool)1)) && (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6c5ad01-0a64-4f40-9baf-ad1680e8ebd5
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    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: 7ddead7a-818a-45ad-b857-8a9ee573f394
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    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: d07c6a2d-f502-4e1c-aa2a-86017f927f65
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 42d7970e-f787-443f-a1b6-fd6b2bcc4086
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fa1cc42-f27c-40fb-a81b-935677c7c163
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8964a81-46e6-47e7-a16c-248ff33de7b7
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd062d88-543d-4240-ab53-7f9b217e2744
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    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: b24cf0d0-065b-4cc9-b9b7-ef9dff256024
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    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: 1026048a-ccb7-4bd7-baa5-5a7221cb3079
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EBX && __unbuffered_p0_EBX
      <= 1) && (__unbuffered_p0_EBX == 0 || __unbuffered_p0_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d46425b-9262-41e3-a812-fc226974b5a2
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p0_EBX && __unbuffered_p0_EBX
      <= 1) && (__unbuffered_p0_EBX == 0 || __unbuffered_p0_EBX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8cc55bb6-4db8-4a9d-912e-18cea25ef903
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 1) && (y$mem_tmp
      == 0 || y$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e29ebe6-a0ae-43ce-93f5-93efec0c8cc9
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 1) && (y$mem_tmp
      == 0 || y$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b96f675-88b7-4339-9aac-c7dc38f397b6
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice0 == (_Bool)0 || weak$$choice0 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05c1cdd4-41f3-4dd9-b630-e1d736821865
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (weak$$choice0 == (_Bool)0 || weak$$choice0 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abfbf214-1d8c-43b9-bd82-b541d126c3a7
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    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: 801a4157-38bf-434a-a9ae-f5318ac3ffcc
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    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: 7739b626-0c42-4ead-9bba-dc332256c65a
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db0a1f17-7e28-413b-bff4-2d5317121931
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4916a631-9d51-4d4a-bd40-a7c8abed455d
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$r_buff1_thd2 == (_Bool)0 || y$r_buff1_thd2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6dc038c-8d85-429e-b8e7-4d4452acf9af
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$r_buff1_thd2 == (_Bool)0 || y$r_buff1_thd2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34abbf06-8e55-470b-9c30-88e2eb29ef73
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff1 && y$w_buff1 <= 1) && (y$w_buff1
      == 0 || y$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 626de92b-68f9-4fec-8466-d7195154118e
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y$w_buff1 && y$w_buff1 <= 1) && (y$w_buff1
      == 0 || y$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68f69c66-da64-4fed-b101-d68da7e9cfeb
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$w_buff1_used == (_Bool)0 || y$w_buff1_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19f19d4f-93d6-444b-ab2a-f0062d21edcd
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y$w_buff1_used == (_Bool)0 || y$w_buff1_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37f23d13-5899-4ef3-94cd-32257729d610
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 826
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe5841c3-f98f-4e33-9010-3bfdb8740cfa
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 8bca3782-e37e-4464-913c-4b47ba4bdab8
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 51ad488b-792b-4bcb-bb22-d61d892ddfab
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 772
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1802b258-8eef-4ea3-b2d3-7d22d6dd4a8a
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 800
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 12bc2a13-e796-40c8-8b29-181bfc64f22c
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 751
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 50af78ca-87ad-4f80-8d7b-015bcabffa74
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 806
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c1ca9724-5a4b-4451-835c-22d14aa7e2e6
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 791
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a4f15792-9fa9-417f-a123-e224e463e6b4
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 829
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 29e1d5d0-233e-4f5f-9e56-40c994e9e3a2
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 837
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: cf910f7e-4a5b-47b2-9b99-32ae7c01d171
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 831
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e5813c51-2489-4e06-8aea-ffecb081802c
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 797
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2bd63459-0d81-47c8-a9c2-f3ec51f41d7c
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 840
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2769d436-36b5-4e7c-bada-591c928efe96
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 773
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 99ffb2e7-628b-43d6-be79-9086bd8315ea
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 780
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 83bfa854-01be-4649-9d0d-aad63787ead7
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 790
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e9fe4f80-331c-485f-9004-739766bd84b7
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 754
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1aa55d85-61b0-4a6d-b8bf-dbb49957fc05
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 799
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6c3092a9-90df-4ceb-8788-69f8577af193
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 809
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1d20b774-416d-4739-b621-46abb69491a7
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 827
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 8eecc100-2d55-4dd1-9219-eee5b0155f5c
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 775
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 4f7b10a4-e89e-4899-a0fb-48108d168914
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 752
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 09b41ef1-a75f-4207-886e-8af0bff19f95
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 807
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: fe481a79-077e-49c9-be77-400c2420631e
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 796
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 64233651-bfb8-4340-9a7b-05aef8401628
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 748
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: b46b8eeb-2f01-499b-99a9-981b582b9a48
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 749
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9ab5cbb4-0a2a-459a-992f-e45bfab23906
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 838
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6da98914-983e-48a4-aa07-d44274296cad
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 771
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 2ded443d-84e3-4041-bf6b-bfe444290b48
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 746
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 7a8493c5-0b95-4f47-8655-a3d3afc4fa10
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 794
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 47c9bba8-7daa-4fed-be2d-8db00684d714
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 770
    column: 3
    function: P0
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 1b19b929-0cfe-4d19-a286-c1549ad6529e
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      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: d716a9df-6659-4ea8-9db6-269e5793963c
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      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/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 824
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 6da44a15-fafc-4d72-af5d-a7e92c338644
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 793
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e1db6acd-a5e4-4ae2-8dbf-559b83cd3d9b
    creation_time: 2024-04-26T10:41:26Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix031.opt.i
    file_hash: 526111e98fa506d5405af18114114ae6aa9ce1a2e8442e7719052c05a249c119
    line: 755
    column: 3
    function: P0
