- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 350d7f52-e592-441c-ae54-bfb856b8a133
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 698
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (B_locked || ((((((0 <= g && 17 <= g) && g <= 42)
      && g <= 127) && g % 25 == 17) && g != 0) && (g == 17 || g == 42)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14899d68-e1db-49d3-99ef-70d89a49c215
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 698
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((0 <= g && 17 <= g) && g <= 42) && g <= 127)
      && g % 25 == 17) && g != 0) && (g == 17 || g == 42))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2a167df-acd5-4b3a-9ced-16d3b48f1554
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 698
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (A_locked || ((((((0 <= g && 17 <= g) && g <= 42)
      && g <= 127) && g % 25 == 17) && g != 0) && (g == 17 || g == 42)))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 2a807138-de79-47f1-8f95-2bdfdc102b49
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ac473795-6889-4ad2-97e6-6f70db55f3a4
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 690
    column: 3
    function: t_fun
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: e9971732-8b8a-4c6b-b36d-49a655108896
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      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: 4f556384-967a-4900-8e7c-85fda6592cd8
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 697
    column: 3
    function: main
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: aaf450b2-d073-4e4d-82c1-f77307f6e6c2
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 166eca70-078e-482c-886a-a9c0a1636674
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 687
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: d1597184-784a-41fa-ac2b-90a60e91c5b4
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 689
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 891facb3-363f-4e63-9286-ebdb16cfc7bc
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 702
    column: 5
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 12433041-4c44-4966-879d-b9ec46baf0ea
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 703
    column: 5
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: db9cc80d-e5fb-48f6-a4e5-93a381a02aa5
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 698
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 047ef12e-f01f-42ff-81f7-36d38de1c2d9
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 707
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 5230e5af-d2d9-4992-b86a-f973c4abcd4b
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 686
    column: 3
    function: t_fun
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: f47d000d-1a73-4045-b4c4-45ffa9950d0b
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: B_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 699
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 24161768-1f18-4311-bcae-aa176ebe5ee9
    creation_time: 2024-04-26T10:50:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: A_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/36-apron_17-traces-rpb-litmus_unknown_1_pos.i
    file_hash: dfa09ef2a9611ca17b7987ae6667bf9c5dfecc9a3d2f86327d9d054dda20e42c
    line: 708
    column: 3
    function: main
