- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 1d82bdb6-4d6c-4271-9a4d-070d9d4974be
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || x$r_buff0_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 4117c738-a59a-4c9e-8d51-160215ea3a30
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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: b34928ba-8d0b-44c9-b890-eb0a7fa7cbd8
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: c69cad48-90ae-437b-8db6-4c41da1e1962
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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: f2e883f5-12cf-40ac-87ad-c7725a073daf
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= x$w_buff1 && x$w_buff1 <= 1) && (x$w_buff1
      == 0 || x$w_buff1 == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 9578f216-9d45-46e6-b06f-9d6c936db96a
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (x$r_buff0_thd1 == (_Bool)0 || x$r_buff0_thd1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 289bca4c-301d-47cc-a013-6042c467b240
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: dbf71bc9-89ef-4bc2-8c28-8b7b032c6ace
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 74105941-0a0d-4719-be09-c490f52bd4bf
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (x$w_buff1_used == (_Bool)0 || x$w_buff1_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 3ad2c81c-fb35-4b7e-a348-b9bde899bf86
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= x && x <= 1) && (x == 0 || x == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 69bdca95-cfde-4974-87b6-52a1d552bbe9
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= x$w_buff0 && x$w_buff0 <= 1) && (x$w_buff0
      == 0 || x$w_buff0 == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 4c312854-c65e-4092-a0ea-4ced0ce7d751
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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: 12826866-4065-41e4-b481-33e5284a7cf4
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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: 5f8a148b-8527-469e-b41a-dbd0a73248dc
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || x$r_buff1_thd2 == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 2d6b4eb5-a007-4cbe-84c0-596ae3e2a357
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 1) && (x$mem_tmp
      == 0 || x$mem_tmp == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: caa8a22f-e597-47cb-a2a8-fde6a2c0e697
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (x$r_buff1_thd1 == (_Bool)0 || x$r_buff1_thd1 == (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 4affb17e-5a10-4393-9a3f-7cde49c05140
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: e58465ab-6145-4530-b0da-beefaeb48e4d
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (__VERIFIER_atomic_locked || x$flush_delayed == (_Bool)0)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: a9490ee6-0b58-402a-9d69-f05b855f4cf7
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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: e40486b9-9421-4c91-a48e-eb3210079a67
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EBX && __unbuffered_p1_EBX
      <= 1) && (__unbuffered_p1_EBX == 0 || __unbuffered_p1_EBX == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 79ae6e3e-6684-4024-afe9-c06fa9f3206a
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (((0 <= y && y <= 2) && y <= 127) && ((y == 0 || y
      == 1) || y == 2))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 0a15ce4b-7881-4ea6-9e9b-ea817e509a8c
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (x$w_buff0_used == (_Bool)0 || x$w_buff0_used == (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 31c92ca6-c510-4100-8345-5d824c63af9b
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (x$flush_delayed == (_Bool)0 || x$flush_delayed ==
      (_Bool)1)'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 61c25c53-c5ca-44a9-a9e3-7819030952a3
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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
      <= 2) && __unbuffered_p1_EAX <= 127) && ((__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1) || __unbuffered_p1_EAX == 2))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "2.0"
    uuid: dbd7e741-cf35-456a-b526-33041123b561
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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: 8b623997-a58d-4375-a055-7bf671cedf67
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 811
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "2.0"
    uuid: 6210f49d-9306-4418-a30f-820e8c815641
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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: 62695479-6fde-4ce9-88b7-fd7ae5aad2be
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 825
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 55e5c047-ceb4-4677-922e-bb0669d86efa
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 758
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 1c1074c9-c8bd-48ca-b38e-4ed6fe6e2fdc
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 786
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 8f0a2518-2f65-447a-a0b4-3b7b04613981
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 751
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: ec711e98-b4f6-45b7-bbf4-e7943fdeb2ca
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 771
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: fe8868b3-a37a-42d2-bcd7-3fd41ad02f40
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 750
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 122a9e6f-3597-44de-b6ce-346ba84d989e
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 793
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 973f5b71-de27-4069-b012-18462b2228b8
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 787
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 641b1dba-11de-4e12-b5d3-6b8d65126433
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 765
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: b4cdb8e2-002a-4af7-a343-82c4710d8e3f
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 818
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 5dfaf982-8d50-4e61-9fa0-ac18e207b4c9
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 767
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 7bf125d8-07d4-4067-ac52-51cce70705b2
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 747
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 61fc171c-1d0f-4226-8c06-71a0bb45190f
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 770
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 121df309-20e5-473e-ba6a-941a61a0178e
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 796
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: a24be70e-6650-40b6-a1a8-c66897258d7d
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 760
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 35f42187-172d-4e48-9e61-4d254b96fafd
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 824
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 213e3375-9bbf-4b9b-811d-10c561a80e62
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 757
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 84880cde-cb0a-4579-95a9-affff106f27a
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 768
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: ef071e4e-e3ff-4f26-ba45-5abed0ad2648
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 737
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 411e4bf2-90cc-4ae5-89ec-f7b1804dc28c
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 748
    column: 3
    function: P0
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: d89449fe-e681-4a11-9890-b0b75e1cc47a
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 814
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 9fcd1ab1-140b-43cd-b872-8acb548fdc09
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 816
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 561d2c2e-0ba3-4a48-8a36-b7112638ee95
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 794
    column: 3
    function: P1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 9a305ba0-313b-4b9a-a74b-68e40f9ce722
    creation_time: 2024-04-23T10:55:12Z
    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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
      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/rfi007_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i
    file_hash: 60cd4209446f80c263553fdb6a481b4dd4e668058f5fe80fa8786bdb8310f6e8
    line: 827
    column: 3
    function: main
