- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: b276a012-f7d2-4c7b-b461-880c41e5aeb8
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: d1e23380-534e-410d-837c-e754c94de0fe
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EBX && __unbuffered_p2_EBX
      <= 1) && (__unbuffered_p2_EBX == 0 || __unbuffered_p2_EBX == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 5257cbcd-6235-4bd0-a7f3-30979243adb4
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (main$tmp_guard1 == (_Bool)0 || main$tmp_guard1 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 7a49ccfc-3614-487d-a1ce-c8d69d1a1c91
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || y$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: c8d3ca13-91c5-418f-a3f4-d49566dd437b
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || y$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: f02b7631-82e8-454d-86ec-99900027013e
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (weak$$choice2 == (_Bool)0 || weak$$choice2 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 28700a71-0b95-42ff-9130-198a482b5b58
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || y$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 05c5c851-4756-48e2-9bbb-a7d01a39a4e2
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= y$w_buff1 && y$w_buff1 <= 1) && (y$w_buff1
      == 0 || y$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: be66f88b-17ba-45a5-bf0b-a7bf7eba320b
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || y$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 21bf9982-83f4-42fb-984e-b3602e4ed9d5
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (main$tmp_guard0 == (_Bool)0 || main$tmp_guard0 ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: eab4f6fb-ceb9-4487-aa7d-6b11b3ee3c3b
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (y$flush_delayed == (_Bool)0 || y$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: fbf1420c-2349-4792-aae3-70692d7f32b9
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (y$r_buff1_thd3 == (_Bool)0 || y$r_buff1_thd3 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: c9207cb0-c358-477d-9687-7c49fa666f47
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || y$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: a4af21cd-27fe-4314-af3b-87754eeb77cf
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= z && z <= 1) && (z == 0 || z == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 142cedae-9d0c-4ef8-87e5-8271a9c1cb0f
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: ffdec62c-505f-4f20-8678-c983b590b1a9
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: be011415-37df-4d49-bbbb-53267e9212f1
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || y$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 5fab5873-fdd7-4b03-9854-622e2c9cac85
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (weak$$choice0 == (_Bool)0 || weak$$choice0 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 4b7ed81e-68d2-4a9f-837f-004fa2b508dd
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || y$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 2bae583d-c7db-4d87-8333-a5ceb941a459
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= y$w_buff0 && y$w_buff0 <= 1) && (y$w_buff0
      == 0 || y$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: a68e4da7-afe1-4ea5-b6ec-bf6414d1357f
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= y$mem_tmp && y$mem_tmp <= 1) && (y$mem_tmp
      == 0 || y$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: b4c4e4e0-ad80-4cbe-b9cd-ca362bb8a7f0
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (y$w_buff0_used == (_Bool)0 || y$w_buff0_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 989b33cd-245d-4d9c-a81a-50c3e8d25437
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p2_EAX && __unbuffered_p2_EAX
      <= 1) && (__unbuffered_p2_EAX == 0 || __unbuffered_p2_EAX == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: e211b302-6fb1-4de9-a284-54524ec9a273
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 5c35f717-a6d6-4421-aaa3-5906ceebca71
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 190975cc-4b65-4b38-95ad-5ef2dc66abc9
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || y$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: a038aed1-deac-46ca-b527-ab2ea25013be
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (y$r_buff0_thd3 == (_Bool)0 || y$r_buff0_thd3 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: e28073bf-fbc3-4234-b769-d4e04b5d501c
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || y$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 039c370e-990b-43dc-8578-bfc146ec636e
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (y$w_buff1_used == (_Bool)0 || y$w_buff1_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "2.0"
    uuid: a7b57ae5-7985-4da0-b0ee-b12b270a5c2b
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: d7215597-fcd2-4e9d-b8d9-7bf45c9bba27
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 841
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 598e149e-e62e-4573-80ac-77075363d392
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 806
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 332ea217-0be9-4806-a51e-601cc78866ba
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 800
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 6d34c698-6dba-47c9-a4a9-318bb6e2b326
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 751
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 08dd39ff-89d8-4fcd-9d4f-0354f8d44a6f
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 804
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: f2387a2e-a827-47cf-a9f9-9a3a456a65f2
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 810
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 8c992a43-ed1c-4a1b-b9a6-df806b619612
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 852
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 64d9e6c4-820a-4349-aaa0-ecd8a1aa8a7b
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 764
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 2564ef99-94cb-4e38-8fc5-0688b6381cde
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 807
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: e944f2cc-788e-43c6-afcd-1ed6805542eb
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 839
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 649c0c0d-cce7-4363-8ca1-9a71fdec6762
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 780
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: c0f3266f-0462-4ed3-bec9-98313f81eb9a
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 761
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: d35525da-8ba2-49a1-8704-6a6001845cee
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 763
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 6c40ac52-d65c-4db3-82dc-482187b30315
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 754
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: f0fe9283-3d1f-48ac-8e4e-0693b548eadf
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 801
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 03ee3bf2-94dd-407e-9d22-56db881a57a4
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 809
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 22b4d318-86c8-45f3-9b09-48a73214375f
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 756
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 9eabb126-1350-465a-842d-f75e040c0ab4
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 819
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: ca659282-6029-4f3e-a674-82135bb48a88
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 752
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 64614228-fded-4ffc-a890-eb3bf46b8e66
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 781
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 12656916-9c48-4a3e-a0f5-2b069e246ea5
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 784
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: bfe92f7a-f6b3-4145-8774-b102511410f6
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 789
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: c4fa6450-2c8e-4903-bd10-a137db8f8e79
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 748
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: c15f579b-d0a7-4a2c-8c91-49a7d88b0efd
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 779
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 616c83cc-4a94-42db-9263-1e320fedea42
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 749
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 49581b16-4181-4de8-a645-e082d89c4505
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 816
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 911e7b74-2a21-44b2-b85e-3c170f656d60
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 782
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 24432e2c-d733-43e1-99b5-40ff039d6409
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 753
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: b718abb7-c9a4-4dbb-8fb4-94ca633eee54
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 843
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "2.0"
    uuid: 18655233-af4a-444c-933f-01393f41c50e
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      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: "2.0"
    uuid: 79ceb928-2182-4f3f-8969-6dd547858715
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      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/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 834
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: a836a5e7-7c8f-41db-88d2-cf3e1559b50a
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 746
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 7eb7f4d8-c662-4437-9c30-5a5ec6cc1727
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 803
    column: 3
    function: P2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 7bf50111-d064-42f6-a397-3a3ef9cd0a27
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 850
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 8810be77-ba82-4ae6-8fc6-91d2a9fb0bee
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 849
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 544179b7-663f-4f1d-8706-645c6f9b21d5
    creation_time: 2024-04-23T10:54:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __VERIFIER_atomic_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix038.opt.i
    file_hash: 8aba011b4454b6464ed30c6424ccbb7bc43e89a3e2bf826373810de7cb8fe97a
    line: 817
    column: 3
    function: P2
