- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f04a13b1-d16d-4184-ac6d-f14353aa3a0f
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: 4294967295LL - (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99abb388-efa2-4aa0-b19a-ac3101615293
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36a80963-f9fd-4f82-a1cb-2505c8193dfd
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f38d2d5-8509-440b-b298-94d114261873
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 143
    column: 7
    function: Id_MCDC_95
  location_invariant:
    string: 4294967295LL - (long long )Id_MCDC_102 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4fffc3cb-4c21-489c-bb64-b786d7e7bbea
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 143
    column: 7
    function: Id_MCDC_95
  location_invariant:
    string: (long long )Id_MCDC_102 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eed963af-d043-410a-93e8-9ece2d4718d6
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 142
    column: 13
    function: Id_MCDC_95
  location_invariant:
    string: 4294967295LL - (long long )Id_MCDC_102 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6a5cb18-a73b-48a9-80af-e77f0f8e5291
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 142
    column: 13
    function: Id_MCDC_95
  location_invariant:
    string: (long long )Id_MCDC_102 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 908b063f-d215-49fb-9a29-e8117e00fc80
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 146
    column: 0
    function: Id_MCDC_95
  location_invariant:
    string: (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: afcd0b2e-4503-4ede-b82b-598467136858
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 146
    column: 0
    function: Id_MCDC_95
  location_invariant:
    string: (long long )Id_MCDC_102 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02dc8a87-e3e6-48fe-9b9b-18af6b6a33ea
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 147
    column: 0
    function: Id_MCDC_95
  location_invariant:
    string: (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 711def7c-72a8-45df-a05b-0a5f0822c765
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 149
    column: 0
    function: Id_MCDC_95
  location_invariant:
    string: (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab35b297-abd1-4a41-ae3e-35653b490d3d
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 170
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9815863-956e-4ed0-9941-e8e5b048c2a2
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 170
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d39a504-8504-45d1-ba9d-3b17f201467b
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 170
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_121 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65b99e76-5315-4f40-a0dd-97b7407fa1da
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 170
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_122 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c457ded1-28ac-4008-8448-9e9573005656
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 170
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25c48320-ee32-487f-895a-47aa895166de
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 170
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e0ba4b7-dced-4240-ab5b-b9ad4dc3accc
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 170
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_121 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fc878dc-536e-4959-89bf-56e9bfe8db31
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 170
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_122 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64706bc6-7ea8-43c6-adb0-5d5e054f844a
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 171
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 645790e8-9c85-4b69-9aef-2dfb4802e52a
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 171
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0bf84c2a-ca86-47a0-a084-b65250c05ad9
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 171
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_122 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c8cbba7-6f55-4e76-a62c-68e69590b1c6
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 171
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07601f02-a112-4793-bc1e-d62b0c0274f0
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 171
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b068abd-4d7d-4fa8-a3f1-a96ab1583f3b
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 171
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_122 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4febb3cd-c380-4416-945c-4079f1dc0de0
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 177
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60a2fa35-803c-4af2-b0e4-23f3622e429f
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 177
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21ef2247-e67f-4ba5-b024-ce5f0e08c42e
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 177
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4e47cb2-68a9-40fc-8aca-0e1d7a2b9a62
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 177
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 438f3ccf-b38d-435f-8060-6990debeee3d
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 178
    column: 3
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea608e1a-8532-4a8d-bcfe-da00f7f8f2fb
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 178
    column: 3
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7927e4c-8839-4f31-beb3-ae14a5425d1c
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 178
    column: 3
    function: main
  location_invariant:
    string: (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fd8f999-6c81-41e5-ba04-f33735e44e3c
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 178
    column: 3
    function: main
  location_invariant:
    string: (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 442bc7c9-5e78-45ac-b112-e886ba5e10d5
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 180
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de8ea6fd-858f-433f-bd87-7f2bd710816a
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 180
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba68fffd-dcb9-4a88-87a5-37c011c2ca19
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 180
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3429cbc9-240f-4a36-bee1-72efefb719d7
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 180
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 569e6fdf-12bb-4e36-af6d-5d3016dd6844
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 183
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 970b9f51-be79-4756-a291-4f3e13fbff63
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 183
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 302184f6-9370-4bc2-9f29-87af8c130b1d
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 183
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e6408bc-4234-465c-83e6-f8c2653e1d15
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 183
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69cbdcc9-ed31-4090-a7db-949f9c30a50d
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 184
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7fac2b87-b104-4cf7-a8d7-bd5186b52f0c
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 184
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2baf9fd7-0af1-49d7-b917-ae6ea2417052
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 184
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a96f155a-6a17-4705-b9d1-61ef4bae54e8
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 184
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_119 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6f2112c-a713-4d17-881b-f0e400983ef7
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 184
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_120 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab85d346-41c2-4247-bde8-6b27f8ba947f
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 187
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: 0 <= Id_MCDC_98
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f3ef345-f0eb-4bf2-9ece-a486cb4cb473
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 187
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: Id_MCDC_98 <= 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: efaba63f-bfe6-44a8-bb1e-6232ee9abeca
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 187
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: (-42LL + 42LL * (long long )Id_MCDC_98) + (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be17d37d-6d19-4c1e-8c9c-40142ba95206
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 187
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: 1LL - (long long )Id_MCDC_98 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9473689c-0386-4127-a694-9ebd5d750369
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 187
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: (long long )Id_MCDC_98 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e4ccf7d-3546-4089-b18d-0ce7802efc15
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 189
    column: 9
    function: __VERIFIER_assert
  location_invariant:
    string: (-42LL + 42LL * (long long )Id_MCDC_98) + (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7c23e84-7305-45c9-ba1c-57cb849cce05
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 189
    column: 9
    function: __VERIFIER_assert
  location_invariant:
    string: 1LL - (long long )Id_MCDC_98 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 082c17d0-eff7-4328-b4c8-a951555abed7
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 189
    column: 9
    function: __VERIFIER_assert
  location_invariant:
    string: (long long )Id_MCDC_98 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d52276b2-b697-470a-8ed7-9411c1a39c40
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 189
    column: 23
    function: __VERIFIER_assert
  location_invariant:
    string: 1LL - (long long )Id_MCDC_98 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 603a1917-82ea-4696-953e-7b1de8ee7113
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 189
    column: 23
    function: __VERIFIER_assert
  location_invariant:
    string: (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25f9bece-1a7c-4baf-aa1e-76239536f854
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 189
    column: 23
    function: __VERIFIER_assert
  location_invariant:
    string: (long long )Id_MCDC_98 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4ee55ed-8d91-4ed6-bd1d-b2b385c78500
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 191
    column: 0
    function: __VERIFIER_assert
  location_invariant:
    string: (-42LL + 42LL * (long long )Id_MCDC_98) + (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4054b3f7-b22a-4881-b342-aa54e8a37ef8
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 191
    column: 0
    function: __VERIFIER_assert
  location_invariant:
    string: 1LL - (long long )Id_MCDC_98 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfb1983d-ebfd-4085-9f0e-5a5ab644fb1f
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 191
    column: 0
    function: __VERIFIER_assert
  location_invariant:
    string: (long long )Id_MCDC_98 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6fef5348-908f-40ca-b352-d81e023e61c7
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 130
    column: 8
    function: Id_MCDC_92
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37b4e7ec-3d9f-4f4b-8d16-89449cf03051
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 130
    column: 8
    function: Id_MCDC_92
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f45f3fa2-2e05-405f-bca8-88a09fa405ab
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 130
    column: 8
    function: Id_MCDC_92
  location_invariant:
    string: (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99171642-625b-4ac1-88aa-e8a7a24e748b
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 131
    column: 1
    function: Id_MCDC_92
  location_invariant:
    string: (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a32c3101-44ab-4829-ac7b-d4cd97040ec0
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 141
    column: 5
    function: Id_MCDC_95
  location_invariant:
    string: 4294967295LL - (long long )Id_MCDC_102 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 451be960-6830-454a-8fc2-929acffde0f6
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 141
    column: 5
    function: Id_MCDC_95
  location_invariant:
    string: (long long )Id_MCDC_102 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a5a7773-713e-40e4-96ce-0ad53ac79915
    creation_time: 2023-01-27T16:29:16Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/aiob_1.c'''
    task:
      input_files:
      - ../plain/aiob_1.c
      input_file_hashes:
        ../plain/aiob_1.c: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_1.c
    file_hash: f089d1b40a76f9af7e090d21489c70b68a6ceb7402496399cd1357670ffd9b51
    line: 144
    column: 6
    function: Id_MCDC_95
  loop_invariant:
    string: (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
