- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 180ef386-c189-4b76-babf-d7ce2bd05a5e
    creation_time: 2024-06-18T15:13:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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/lazy01.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: eb9cf44f-7a43-453a-ab6f-52e61409b38b
    creation_time: 2024-06-18T15:13:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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/lazy01.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
    file_hash: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
    line: 706
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ed9ee313-d1f8-4491-8d29-bfd91c5e0c53
    creation_time: 2024-06-18T15:13:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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/lazy01.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
    file_hash: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
    line: 713
    column: 3
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 02790352-4422-40fe-86b1-8f78d9e70c18
    creation_time: 2024-06-18T15:13:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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/lazy01.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
    file_hash: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
    line: 720
    column: 3
    function: thread3
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 93eb4e69-1fec-4897-b1a3-bdcdc42edee2
    creation_time: 2024-06-18T15:13:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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/lazy01.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
      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: 14134bfc-6d38-47d8-9784-22e2c6df3963
    creation_time: 2024-06-18T15:13:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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/lazy01.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
      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/lazy01.i
    file_hash: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
    line: 732
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ef4c53cf-1763-4738-b1b7-a1804c1dbe92
    creation_time: 2024-06-18T15:13:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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/lazy01.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
    file_hash: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
    line: 708
    column: 3
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: a58acc9d-3a8d-49bd-aa03-fac3dd5fb837
    creation_time: 2024-06-18T15:13:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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/lazy01.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
    file_hash: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
    line: 725
    column: 3
    function: thread3
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: e427c6ba-2418-4883-8afc-effbf0c09609
    creation_time: 2024-06-18T15:13:59Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--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/lazy01.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: mutex_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/lazy01.i
    file_hash: b5d87933b05ad3566f9bc28daac5c0aeceb8a45433a1cac3d51a8d34f7f284f0
    line: 715
    column: 3
    function: thread2
