- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75734700-6e95-46b2-850d-599b6d9b68ea
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      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: 850170d4-5323-49ed-b6d7-f6188a68401e
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      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: b03175b8-2b28-483d-b070-884dc81b8fe7
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      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: 255e803e-9d69-4bac-892f-81cef048f082
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 414c435a-cb28-4f8c-bcb8-0a402f7c8ba5
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 447ace18-ec6b-4d9f-9e44-79e57d625a05
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 4597873e-c517-4068-a901-e9381610ac75
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 7294b010-83c7-442a-9472-44e853b2bebb
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: b9cd13db-e2c5-417e-8ae5-1732c03f45dd
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: debfc7f6-a2dd-4e0b-b385-5f075ae7eb75
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 9625cbfc-bd21-41d9-a0b5-01fffe27c1fa
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: fd188657-e863-4fc8-b2f9-c43db2146268
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: f906250d-ebaa-4a34-879d-0e818b517834
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 5ea78d1e-c0d8-4635-85f3-4f7c3a60853b
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: e719c8f4-6a7d-4783-9b12-4754d6603143
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 8a293923-8bf0-4b88-9a5b-e863b4db8eff
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 43f000a4-1137-4e8c-9f02-9bba33644904
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 1e92ce33-de9d-47d3-89e9-4ceb0fd5ef27
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: cffc7413-8aec-4a2d-be5d-ef22f1c02847
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 1f027031-8a53-4299-b0a5-f060b38fd817
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 45fb09e0-bca5-4906-baf0-dc8a6c2e374c
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: c7683f86-e75a-4dec-9b40-f2695a1040af
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 7c18ac9b-d864-4875-a00b-fcb5b4af359c
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 3b0b0236-7d79-446a-be7b-ac6a759e4e44
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 4dcfbadc-bc4d-494a-b07d-3ca2974fbe2c
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 0a616116-6ded-4abf-ad9c-9ae27b5199f6
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 6c418f83-86fa-4a65-8418-8e77a4b80d6c
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 7e3c947a-7a76-4f09-9cea-f59a7456b05e
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 4a41f1a4-f649-4972-b1c2-b1741bd1b2dc
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 0b999d41-95ee-4d68-93da-68926c6d91bc
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 5446a185-590e-485d-8a62-3ec530cc7daf
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 10280dfe-1d07-4331-b55d-ca4309c914c8
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 685f4304-29ea-4f64-86c7-ecc7729ec553
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 8984000d-15f9-4bdf-a085-72ba9ea5d510
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: d269ef86-be6a-4b19-b772-f6e23750d25f
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 11ac97db-55eb-4893-8e12-2b1372b84f99
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: af1d995f-b38e-4f2e-a5f6-a854de8f6227
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: eaf034a6-ae07-4165-9736-95a901835975
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 8b0479cd-d9b9-480b-9c13-e0fc3b4370d1
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 0e95cc41-7b4a-4177-add7-aa50a1435e7b
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: e1a91c21-ffdd-44e7-ae98-d3b4de637df4
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 30a6a3aa-05a6-4b33-b3b8-296943f78421
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 5ac17da6-3ba0-408a-8510-5975ff7162a6
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: c6861305-1a1f-4b0d-a776-f42fa9338455
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: eef91d9b-1972-459c-b95f-2cb3b185c04c
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 313b7b99-5337-4f43-a9ed-40680ffb1401
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 76271ab0-ff07-4bb5-9311-09e80a8cf677
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 2e122188-5932-40e6-b1fb-4e8196b9de6a
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 6b129310-7085-4114-a872-352d12dcce74
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: f1aaed87-60cd-410a-b72d-ff07b237a67a
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 93ea2a47-7568-49fc-b3f0-1ce100700a2d
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: b8f6de54-3a59-4b89-8eec-0af4cba4c803
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 44a7e925-2dc0-42da-8eb7-31285500832c
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 483952dc-4dc1-4910-956a-8b48fbc0f83c
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: a0f1da73-2cb2-442e-99e6-794a1b69ba67
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: c06ead8a-c45f-4a07-9ac0-f9bcde84defe
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: d0b53a29-3e62-459e-9262-a95e00180002
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 6f542275-f6e6-4b10-8e4c-626bf796d843
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: fa15a4c4-001c-4823-a429-0f6f4eebf4bf
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: ea3e7d50-a9d7-47dc-b1bf-f6307c672170
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: e3e71b37-52a8-4084-ac59-b14b98b1f195
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 52526513-e415-416f-adb5-7cfac069bd0b
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 86f5d819-f093-44b7-832a-6d8c2e4e1e04
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 4fa99fab-81e2-4f52-8aae-183ca162f523
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: 2b7dcbd2-6365-43de-bd6a-a77b24d0618b
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: abb1a253-6b2f-4172-818f-5123db5fdce3
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    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: f4defd7a-ac7b-4341-ab12-a22538361a97
    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_2.c'''
    task:
      input_files:
      - ../plain/aiob_2.c
      input_file_hashes:
        ../plain/aiob_2.c: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_2.c
    file_hash: 026c555e7fee0226e2a759c30119467d21d68b18e5fa50b91855a2cfe8505a9d
    line: 144
    column: 6
    function: Id_MCDC_95
  loop_invariant:
    string: (long long )Id_MCDC_99 >= 0LL
    type: assertion
    format: C
