- entry_type: ghost_variable
  metadata:
    format_version: "2.0"
    uuid: f59dfcd2-8ee4-42fa-8119-d186c603a05c
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 501f535c-fd94-466f-990d-0990051fc3ca
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 715
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 49c2dc4c-6311-41ba-9445-6b65d812f010
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 717
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "2.0"
    uuid: cd893bd6-9a5f-402e-a2f2-07dc0012e581
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 15c2270a-e187-45dc-a1c0-0c8919de97bf
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 714
    column: 112
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 78baf344-e969-4d1e-a763-c641a13b2f60
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 703
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 1bef9f81-6b8e-48c6-bd8a-ec409c41a76b
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 704
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: df1f75e0-500c-4204-a7fb-586587103276
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 708
    column: 15
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "2.0"
    uuid: d8de3306-1763-4c51-8083-080b75e180da
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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: 41826625-8d55-4ac5-90d1-3e13782f4a40
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      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/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 713
    column: 55
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 178211f1-89ff-4bc0-aa5d-96868bfe301e
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 708
    column: 114
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: b837b0dc-9574-415f-81c0-ceaa0a64ce3d
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 708
    column: 58
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 90c303a3-8b2d-4486-9a5b-ab462db85470
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 708
    column: 157
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 3492ab1a-9d19-46c0-8a15-e144ea2c7da9
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 716
    column: 73
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 002babd0-4e13-4b2d-b119-7d7035b046e5
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 707
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: d7f7acec-0f5b-42c2-9cda-5f6a0214b899
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 701
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 39408f2e-9966-4612-9679-2e1abba08036
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 714
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 194cb432-f348-4bd1-bfc8-3cc33dc1c50a
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 714
    column: 56
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 4c944ae9-850f-4123-a5e7-9e3dc6d3f814
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 706
    column: 5
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: a7475dc0-bec2-4845-959b-7a7fdc53b3d6
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 700
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 5b61a8f0-09fe-4429-8c8d-25e1ba95bba2
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 714
    column: 155
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: d854758a-4d1d-4fd7-9f71-08f149e1c7cf
    creation_time: 2024-04-23T10:58:05Z
    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/goblint-regression/28-race_reach_61-invariant_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: __global_lock_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_61-invariant_racing.i
    file_hash: b4399e58ed3ca9c75e2a61372e91a4308548a0e79a3eb4428d85990bd71242f7
    line: 716
    column: 8
    function: main
