- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71a7fdef-6969-4955-b147-c9ca7b469746
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 137
    column: 7
    function: Id_MCDC_89
  location_invariant:
    string: 4294967295LL - (long long )Id_MCDC_96 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f62a57b-336d-4722-a1cf-02abf8862ca9
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 137
    column: 7
    function: Id_MCDC_89
  location_invariant:
    string: (long long )Id_MCDC_96 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 914586ae-173c-45be-84b0-ba90631b66ad
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 136
    column: 13
    function: Id_MCDC_89
  location_invariant:
    string: 4294967295LL - (long long )Id_MCDC_96 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c460476e-831f-4fb5-8659-97fb04382253
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 136
    column: 13
    function: Id_MCDC_89
  location_invariant:
    string: (long long )Id_MCDC_96 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11bd8d5b-1cfc-4ca8-899b-9572208adbaf
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 163
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9422178b-4f5c-4592-bba2-55e260e21768
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 163
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a0580e4-ebc7-42ba-97cb-f7011cb87f65
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 163
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_115 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a09d0880-b8a9-437e-b7c9-de91807747f9
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 163
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_116 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0bcecabb-7510-416d-9701-23a7dede1e9a
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 163
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebc730de-b822-42ce-87e0-a4e35f16467c
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 163
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f968b8ac-33a0-4b1a-9b42-e9eaeb9ddce2
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 163
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_115 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43572477-8c80-41d8-a796-256b1e9c70a7
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 163
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_116 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1eca87b2-38ed-4816-b3bb-ca75c47e2ec5
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 164
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12abd95c-b544-4a3c-a869-641d2dfa092e
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 164
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 235a0a74-51ea-4971-b7cf-a763065bc931
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 164
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_116 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a57de48-e42c-498a-ab54-b83d012fc20f
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 164
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de9e8a8a-b814-4c3b-86d6-f517a3cbfc53
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 164
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26e83530-43ec-4f28-8958-78efb2ddd583
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 164
    column: 15
    function: main
  location_invariant:
    string: (long long )Id_MCDC_116 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a453caf-8231-4f17-a002-cca23b42c9bd
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 170
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c93e5b5-20ea-40c2-b1b6-67f0474339c7
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 170
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eef581f2-122d-4a41-a132-8f602fbeb582
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 170
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c39ac5d3-8a7e-4c5f-8526-166b405606e4
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 170
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f67614d-2b0b-4355-a34f-3ab5f491804a
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 171
    column: 3
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff1d08cc-2023-463f-83fe-b6911cf72578
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 171
    column: 3
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da2ec97b-fa80-42d7-87eb-952d2fc6b769
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 171
    column: 3
    function: main
  location_invariant:
    string: (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8174cb4-e4cf-441f-98f0-913dbdc2ca79
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 171
    column: 3
    function: main
  location_invariant:
    string: (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 631e294a-daae-4d91-a567-e57d33be333f
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 173
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93215957-53da-490b-9361-7479c9e15794
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 173
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36cc1a56-aa4d-4f79-bc83-833a02188878
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 173
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be8f3b9f-a039-4cd3-b622-eff439f96ada
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 173
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 460bde7f-4fb3-4e55-b3b1-e8ce33d964f6
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 176
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b5f15e7-2a79-4205-b617-5f871f50f53f
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 176
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f141638-a9a7-49a7-8200-c5fba73b8e17
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 176
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43a65ce7-4c64-4f9b-8da2-14ac55060014
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 176
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48b2defd-ec3d-4294-b3a8-0409a07a617a
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 177
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ca74a38-8abc-4973-838c-cf0952b598a3
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 177
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ef28404-f0ad-4492-b73f-45816eab9fad
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 177
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_93 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1143aef-39c4-486a-9892-5e744a1db15e
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 177
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_113 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9261eae2-67f0-4d3a-bd0a-1c10caa6413c
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 177
    column: 0
    function: main
  location_invariant:
    string: (long long )Id_MCDC_114 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6e3bd84-50aa-414e-8bd0-e7c1a42c3fce
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 180
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: 0 <= Id_MCDC_92
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5a31cc9-5218-4dc5-a90f-2d80e2fd847a
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 180
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: Id_MCDC_92 <= 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba85eebc-f6fd-4384-ad3b-a538c0a87748
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 180
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: (-42LL + 42LL * (long long )Id_MCDC_92) + (long long )Id_MCDC_93 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e03a24c-1dfe-4d22-8b07-0d255f956cae
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 180
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: 1LL - (long long )Id_MCDC_92 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cc23ffd-bde1-4a95-bb3a-89593a9afb61
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 180
    column: 4
    function: __VERIFIER_assert
  location_invariant:
    string: (long long )Id_MCDC_92 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb04a872-ae4e-497f-9b0a-05ec5f2227de
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 182
    column: 9
    function: __VERIFIER_assert
  location_invariant:
    string: (-42LL + 42LL * (long long )Id_MCDC_92) + (long long )Id_MCDC_93 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89eef0aa-d0fb-4111-b4f9-ae647062401f
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 182
    column: 9
    function: __VERIFIER_assert
  location_invariant:
    string: 1LL - (long long )Id_MCDC_92 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9575d2c9-2dd9-403b-80df-e7e361e21486
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 182
    column: 9
    function: __VERIFIER_assert
  location_invariant:
    string: (long long )Id_MCDC_92 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c76c38c8-759c-4145-8b36-430eaa50d16d
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 182
    column: 23
    function: __VERIFIER_assert
  location_invariant:
    string: 1LL - (long long )Id_MCDC_92 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 405d0011-3d66-4cb2-a6af-5c9b512ae4bd
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 182
    column: 23
    function: __VERIFIER_assert
  location_invariant:
    string: (long long )Id_MCDC_93 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a102710-2a30-4f21-97c8-fd960430a076
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 182
    column: 23
    function: __VERIFIER_assert
  location_invariant:
    string: (long long )Id_MCDC_92 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc457e7f-5552-40bd-b57e-3642af31112e
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 184
    column: 0
    function: __VERIFIER_assert
  location_invariant:
    string: (-42LL + 42LL * (long long )Id_MCDC_92) + (long long )Id_MCDC_93 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd81a460-4109-4a7b-8be0-28a3dbacf9ea
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 184
    column: 0
    function: __VERIFIER_assert
  location_invariant:
    string: 1LL - (long long )Id_MCDC_92 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4a42b4a-6cd0-4d5b-8e69-7e709f9059aa
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 184
    column: 0
    function: __VERIFIER_assert
  location_invariant:
    string: (long long )Id_MCDC_92 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b892c11-8a36-4cef-9c7c-a97a95d87458
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 135
    column: 5
    function: Id_MCDC_89
  location_invariant:
    string: 4294967295LL - (long long )Id_MCDC_96 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05301230-1be2-4e99-8777-ef0beaf687b3
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 135
    column: 5
    function: Id_MCDC_89
  location_invariant:
    string: (long long )Id_MCDC_96 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d0c28870-be75-4782-9a34-35122820c4e2
    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_4.c'''
    task:
      input_files:
      - ../plain/aiob_4.c
      input_file_hashes:
        ../plain/aiob_4.c: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/aiob_4.c
    file_hash: 10491a2ba1c0af8edd609b5028b1f925d0288ec6e0b405ba8250552a6ddb6463
    line: 138
    column: 7
    function: Id_MCDC_89
  loop_invariant:
    string: (long long )Id_MCDC_93 >= 0LL
    type: assertion
    format: C
