- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb1ac41a-f31d-490b-91b2-f757513983a7
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e60f654-4894-49cd-b2a4-56df15748f1a
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4249fff-841d-4978-ad88-ea4c76929af3
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76e2fa95-1ca5-4929-9cd0-c28304ad261a
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32e4a262-3f02-4404-b482-d3d8e55670c5
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e839f41b-6d57-4070-8855-43101aaff509
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a92c344-046f-4b63-8703-b39034af5e55
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14f4e7b1-9d76-44cf-a45c-4ceffc5c6d3e
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7a5182d-4f15-4ad6-b191-086c803ef4d5
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a4d4a36-bb63-4600-bc3c-0bd7ef43368a
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ba28f3f-e82a-4e51-bb1c-3aace5173230
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5be0ac06-2d12-4b1e-821f-4fb7a67c9bc1
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 476a125a-da57-4318-bda9-c53d1927244f
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 007a320f-7905-421f-b226-6118d3de70f0
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9200070-c2bd-4054-961f-d86c96b5909a
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23baa372-8c4c-4e54-8b3d-37d321624bb5
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ec44f4e-0fe7-42b3-863d-6e5936e996ef
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48c2319c-e41b-4766-b230-c5ae53fe01fc
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9bb5bbfa-0789-4c37-a737-a4fca522a057
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff0 == 0 || z$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18f5c730-c947-4fdd-a30a-0e96a69f17a9
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff0 == 0 || z$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 773d0a16-dc63-478e-9cfe-c8240f1ca520
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff0 == 0 || z$w_buff0 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da3c0943-a2ce-4ebe-a9a8-8607234ff951
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a995d941-f161-4b6d-b52e-3656e4eaf3f7
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e15946a3-9c89-46a2-948d-e19a49ece6a2
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b7642b1-2ec1-4d00-8e2e-ea460a837296
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71782c78-b785-408f-86e8-1f3fa1c32441
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 426383dc-c956-4667-b219-9b68202b6bc4
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3e46031-4cf0-41f3-95df-3c0ddf6f8f12
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z == 0 || z == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 52140240-7af5-4ac0-9e21-271c82345fe0
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z == 0 || z == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81ad78d5-61cf-40c7-8ed3-2d98330451a1
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z == 0 || z == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd977542-3f8a-457d-8039-cf82d4895bb3
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5d3ec76-5490-47f8-9db5-4ec5f73bf7c1
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e97d2286-0552-4486-bf72-dd6a3cea4f72
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 235a2227-d6c2-46a8-a77a-2634c427f1d6
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a6cc902-b18b-46e8-8f07-d7586b131425
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77563d40-dc39-49dc-bf8f-b914deb0fac9
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2194575-4ffb-4cce-bb27-aa9dda92b915
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff1 == 0 || z$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a316e6ac-9d43-40f4-9a6d-2b68d6793abc
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff1 == 0 || z$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5a63512-ca12-477f-b9e5-8e8c514df74e
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$w_buff1 == 0 || z$w_buff1 == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9186fd80-d417-4cf6-84f7-e9a8fc5a74a4
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$mem_tmp == 0 || z$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d84a547-ce98-4ac2-9484-b9743bdba30c
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$mem_tmp == 0 || z$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07bd57cf-95c7-4bbd-ba15-097a64436a91
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (z$mem_tmp == 0 || z$mem_tmp == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb9dd327-6ed5-4c6b-ba05-4a9e1fe6879c
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EBX == 0 || __unbuffered_p0_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b493c537-1c38-4545-a010-216baa15c148
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EBX == 0 || __unbuffered_p0_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d16a7f9-7cf8-4ccd-be44-39b5a9b67e28
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EBX == 0 || __unbuffered_p0_EBX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6dbb3692-3789-436f-abdc-ee4063fdb621
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y == 0 || y == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8fa5fd9-60df-4a0a-8a5e-52c8626a7305
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y == 0 || y == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b267182-0c53-4fa2-b7bd-715af09b307a
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (y == 0 || y == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25a8f987-3b17-4520-b7dc-00d9dbc3ccdb
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65439dcd-5dd8-4a9a-8e01-c7cc616e62f9
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58cf72fb-eabe-45ed-a174-e28541942b4e
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p0_EAX == 0 || __unbuffered_p0_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebac1faf-89cf-455a-a8bc-42d717caef6f
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4de94ba-9027-4679-9476-e870c29532f4
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    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: 34a395a4-9446-4bf8-a911-9d2fdd57f48c
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    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: e50dac62-c431-46dc-954b-38808616b524
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (x == 0 || x == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35f2115c-c095-4e9f-99a2-1145ab7d3c8a
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (x == 0 || x == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2b4b9f3-06fc-4a75-91c7-ad41d8df4263
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (x == 0 || x == 1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 184939bf-0dff-48be-b0e7-212e1fad491d
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b969a59-ebe7-4773-bd4e-99c06684ab3c
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f9c77d1-deac-4ddf-a270-47d2ed60fab8
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$flush_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71d0a0a5-6b84-45ff-94c5-f8b3ada6e97f
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10f4ab1e-ddd0-4e59-b035-7829e4a570f9
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3037087f-3e89-4841-83c3-3e3adf772f48
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || z$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 124266d1-d960-4232-ad84-e72faab75c13
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 867
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81c0211c-2be1-4b45-81fd-84932bf1aff3
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 869
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 934a28d0-60a9-40a7-a22a-e565f75d8612
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 870
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX ==
      1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 33abd4cc-9036-4638-8e0e-96427176e837
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      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: c434530e-fba7-449b-90a4-7e9d0d588147
    creation_time: 2024-07-04T11:35:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-eval-0-gc0f14bbe0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''protection'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix001.oepc.i: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
      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/mix001.oepc.i
    file_hash: 54b7204af3591799bdde98d626e5c17b99e9c1ebc668ecbb3e0b1bb3bb8aa3c2
    line: 865
    column: 3
    function: main
