- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 0b281b97-e4dd-4651-b373-5407540f3e35
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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: a6bce0ad-f64d-4255-8735-0df2f6025a33
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= b2 && b2 <= 1) && (b2 == 0 || b2 == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 48573be3-dcc5-431f-87c1-e33c309a0fd5
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (((0 <= x && x <= 2) && x <= 127) && ((x == 0 || x
      == 1) || x == 2))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 8e3f7aa0-ecae-4865-bf4a-6bc2b54b03fb
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= b1 && b1 <= 1) && (b1 == 0 || b1 == 1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: c17292cb-222e-40e5-8538-e1f2e303e8e1
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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: ghost_variable
  metadata:
    format_version: "2.0"
    uuid: 9e8042aa-74f3-4185-9eb2-0353521b180f
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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: 64fd3f58-0467-4a63-8973-6cb3fd95363b
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 808
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: ee5ee5a2-4092-4ab9-813c-710211b52996
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 722
    column: 17
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 72daa53d-c06f-4612-abe0-f66e0c5c2629
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 733
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: d2cb8818-f48d-46ae-a139-74496a6f0c31
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 837
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 078377a2-4b94-441c-b98b-fd8ff2bc170c
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 792
    column: 17
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: cfaa7a24-4f99-40c7-8472-73593212891b
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 754
    column: 21
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 04eb95f9-b6be-4f45-a91c-1957759cb7ad
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 744
    column: 17
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 50300584-6edb-48ec-97b8-2b2beba3b81c
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 724
    column: 17
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: f64b790d-109b-4a04-8537-e1627986f1b9
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 812
    column: 17
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 2cd4ac59-2bee-4730-a663-d8a7743e3586
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 814
    column: 17
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 88f74084-72e2-43c7-8692-20380ac7252d
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 838
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 04a1a340-5ad7-4096-ace8-27c21cbf0dbb
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 710
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: a6a6db5d-a7a9-4c75-8fa8-b78d20a72c63
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 794
    column: 17
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: c4aff489-c087-42c1-8094-b680c3c1b184
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 824
    column: 21
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 1afa58a1-c00c-47ce-9916-130d4f4270a4
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 731
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: a6ef63a1-2bf6-4137-9552-d4bab182c2f7
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 807
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 0d492900-c3da-48cd-a6eb-28c0db731c22
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 765
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: ee2deea7-244a-46d5-a09c-3fff87f1cfed
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 742
    column: 17
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 4d4a07a2-5db9-46d0-92fe-c9060e34a0de
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 746
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 6a37e014-d78a-4e67-9233-79878fb2f14d
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 750
    column: 17
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 73fd3466-7021-4f2e-952f-fd2f4991dde8
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 826
    column: 21
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: a7c1327c-9128-47b6-8ebb-4839ee71f30e
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 756
    column: 21
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 79507571-ac7b-466a-a56b-8eae78451a34
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 835
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: ccdfaad0-97c4-4111-aa7b-f697c1f60650
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 738
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 7a004ed1-a8c8-460d-a76b-f8361ac363ea
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 768
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 1a8c3fac-1e8c-44e4-9663-7097b11e76a5
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 801
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 08979642-e2e3-4891-b535-593cb245eae2
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 822
    column: 17
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: cc12d75e-abf7-4740-8ded-0876ff0eed52
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 705
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: c5cd160e-e767-4898-9886-398de0decaeb
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 718
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 9166d007-152d-4284-8a92-d95e282c80d6
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 720
    column: 13
    function: thr1
- entry_type: ghost_variable
  metadata:
    format_version: "2.0"
    uuid: c26f4a9c-6705-4149-b859-f1312c5162db
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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: c1f505dd-8635-4314-8880-ef58eb088ec0
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 845
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 793d7309-b812-4688-9c8c-f9533c5a653a
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 715
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: b8a75289-311a-44f2-a434-9cec2623c75f
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 775
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: f2c8e184-ad37-4a38-9753-44b5cc108b55
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 785
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: c03eb091-fe5b-4ca0-88b0-8b54684d978e
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 798
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: bb7e87bf-ae1a-4dec-8787-9a6d7f3af5b7
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 708
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: b2ba8072-9b2e-4ed4-b15d-e857eac2c490
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 735
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 0aec566b-5367-4e75-aa0d-7f63c0f2c000
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 783
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 4f1ef1fa-11dc-4a66-b129-6d6aa4ad3b21
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 728
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 2220f502-1f56-409b-8776-3c662b15493c
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 781
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: accb7c31-0d95-481a-9d34-36d82c54bd23
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 810
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 5d3e3246-4ee0-410e-b210-aec51a088c32
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 803
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 5b3f2206-3b45-466b-90fc-6f837f3868d9
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 787
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: da187977-096c-45f2-835e-067d145597e5
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 790
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 88092252-b93d-498e-b8f5-94a2816a7a1f
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 788
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: a4100a17-2288-472a-886e-602fca0f4c9b
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 737
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 274ed468-de2b-44de-9cd8-48cfac3e3f25
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 770
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: dcac8f92-c152-4deb-a914-5503da2eb15c
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 767
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: d31a20eb-7759-4bab-8085-7778a7225e95
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 800
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 11964444-4ae6-45f1-bc89-2d282fde3c45
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 730
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 3caf30d6-8ab7-4ca5-ae77-d4bf3414d37a
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 711
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 10588b49-5ffc-4814-b1e1-71d19fe3cbb3
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 818
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: a74a8c7d-a61d-4f79-b220-65fb4beede9e
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 777
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 6b7dc8f9-0004-40f1-9ff2-890d94beac10
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 840
    column: 5
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 28bb56b0-911a-4638-8d1a-c3817c0660de
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 748
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: a5a9e3a9-b3f0-413e-bd44-5f77141dd886
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 752
    column: 17
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 24365bb7-3a3f-4e0a-a62b-3c87a2051175
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 780
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 9303de85-f6dd-4705-89d8-153e11919d27
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 778
    column: 9
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 0cfcd3b9-1eaa-427b-8637-3e1137f842a5
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 820
    column: 17
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 1ff9f6bc-5a7f-4044-80e7-1fd4cc601301
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 707
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: ff3238b3-78e6-4931-b765-91b692af0817
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 713
    column: 9
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 73f1a0af-d2f1-4528-b972-374dcbc6b572
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 717
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 194cc5be-b50e-4ff7-a6d8-e34165734b42
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 740
    column: 13
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 4e504cdd-f569-4129-97b2-9b7bf4f15c4b
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 805
    column: 13
    function: thr2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 93428c05-bc8c-423c-bdb5-2270f2f731eb
    creation_time: 2024-04-23T10:50:52Z
    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-atomic/lamport.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport.i: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
      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-atomic/lamport.i
    file_hash: c35b909c90b92e30d40b0275e3d226db26dbebaf39dc73a31d7e72eee871d214
    line: 816
    column: 13
    function: thr2
