- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 90c74c76-8382-47dd-833d-e1464158e04f
    creation_time: 2024-04-25T07:35:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
      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: "0.1"
    uuid: 261e3637-aa8f-4923-a85f-901408d68297
    creation_time: 2024-04-25T07:35:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
      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-ext/46_monabsex2_vs.i
    file_hash: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
    line: 707
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: aabb37e2-c74f-4aa1-bfb8-c577566d8749
    creation_time: 2024-04-25T07:35:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
      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-ext/46_monabsex2_vs.i
    file_hash: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
    line: 709
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ca30b1ac-f876-4167-ba46-4c1f5a1e8054
    creation_time: 2024-04-25T07:35:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
      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-ext/46_monabsex2_vs.i
    file_hash: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
    line: 704
    column: 5
    function: thr1
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 7aea6f6f-857c-4f73-ab3b-c4b1c62cf8d4
    creation_time: 2024-04-25T07:35:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 1ed48bf0-bcd8-4636-a286-9dc7b2153c95
    creation_time: 2024-04-25T07:35:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
      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-ext/46_monabsex2_vs.i
    file_hash: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
    line: 718
    column: 12
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 3d7e13d5-6c7b-41d9-ae86-565869c2b117
    creation_time: 2024-04-25T07:35:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
      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-ext/46_monabsex2_vs.i
    file_hash: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
    line: 712
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 57451247-b433-4088-9536-58c487a410aa
    creation_time: 2024-04-25T07:35:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
      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-ext/46_monabsex2_vs.i
    file_hash: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
    line: 710
    column: 5
    function: thr1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 581e0e70-a481-4a54-9bd4-ccd2596c7feb
    creation_time: 2024-04-25T07:35:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--sets''
        ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/46_monabsex2_vs.i: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
      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-ext/46_monabsex2_vs.i
    file_hash: 134e9604c8f91a200c8250c9fbb45867ed525dc78e65c16e0a5fa44f5d71ac67
    line: 706
    column: 5
    function: thr1
