- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca21fe3f-0bff-4ee9-9215-ae6b33ae6f2a
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )x1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f47e59a7-c140-4922-900d-44c99146d7a0
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc0549c2-3641-42ea-be96-6af2477c581f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c06fbcc-90de-43f5-ad73-283462620981
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 8
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95bced15-6ecb-4aaf-a6e6-1b6777592920
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 8
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce1aa26b-844d-45cd-80f1-384c977ef5af
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 12
    function: main
  location_invariant:
    string: 1U <= x1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 615d98d5-8d48-4bff-a56e-426a6a4bc95a
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 12
    function: main
  location_invariant:
    string: 1U <= x2
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b92b786-6952-4017-8893-7a86b67b38a5
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 12
    function: main
  location_invariant:
    string: 1U <= x3
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0dacd91-718a-4e13-8dd0-53b1349d1b01
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 12
    function: main
  location_invariant:
    string: -1LL + (long long )x1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cdc85475-48bd-4c4c-936c-5879636e15ba
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 12
    function: main
  location_invariant:
    string: -1LL + (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37716bd9-a2c2-4045-aa20-730f70abbe27
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 12
    function: main
  location_invariant:
    string: -1LL + (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb418906-26a1-454b-879a-fb3425e7c7c1
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 12
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df2ea004-1fd9-40ff-bb9a-8cd90089300b
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 12
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a60a5e6-c8f8-437b-ae00-bd09dbf6dcd5
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 12
    function: main
  location_invariant:
    string: x1 != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4cab1275-6bac-4b74-9be5-b23532b6c7b5
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 12
    function: main
  location_invariant:
    string: x2 != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8bde4d5-3620-4831-b22f-d9bee3b1a183
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 22
    column: 12
    function: main
  location_invariant:
    string: x3 != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2d4d9a8-f5b8-4da6-a094-fb90b7f1f31f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 13
    function: main
  location_invariant:
    string: -1LL + (long long )x1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20852ebb-cfd1-4ff3-ba94-e3c004471380
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 13
    function: main
  location_invariant:
    string: -1LL + (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca53197d-98f2-4f17-99b2-5386510814a6
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 13
    function: main
  location_invariant:
    string: -1LL + (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebe50b00-d22f-45fb-9198-4c20355a26dc
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 13
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af9e54bf-f3cf-44ba-bfd7-04d6482136ec
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 13
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f226c881-60a7-4f25-a257-93329f847a0b
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 17
    function: main
  location_invariant:
    string: 1U <= x1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82c582ee-fa7a-44f0-b58f-b4deb9e26b79
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 17
    function: main
  location_invariant:
    string: 1U <= x2
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c34e922c-a407-4e9d-9b6a-5ecf956ce00f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 17
    function: main
  location_invariant:
    string: 1U <= x3
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ce0e8b1-1c12-4ee9-be98-af248d4a5927
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 17
    function: main
  location_invariant:
    string: -1LL + (long long )x1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6451b34b-51b8-4479-90b7-e223cb02f3ea
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 17
    function: main
  location_invariant:
    string: -1LL + (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd99d278-d574-44e7-b722-a95bbbb692cc
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 17
    function: main
  location_invariant:
    string: -1LL + (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bc1c7b0-1c81-4e37-a0f5-a2b10e851ebf
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 17
    function: main
  location_invariant:
    string: x1 != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0907636-9554-4fdc-bf8f-5eb394fbee39
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 17
    function: main
  location_invariant:
    string: x2 != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4acd6c3d-e784-4e47-b756-5b36bc66eb3b
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 23
    column: 17
    function: main
  location_invariant:
    string: x3 != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7f590a6-b218-42a4-bfb5-5e14ce095169
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 24
    column: 9
    function: main
  location_invariant:
    string: 1U <= x1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fac55c21-4583-4ef0-8328-bd5800044ab7
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 24
    column: 9
    function: main
  location_invariant:
    string: 1U <= x2
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5117f7b-fa79-45ac-b72c-081cc22dd3c6
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 24
    column: 9
    function: main
  location_invariant:
    string: 1U <= x3
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27929d17-bc42-469a-84ac-35faae852488
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 24
    column: 9
    function: main
  location_invariant:
    string: -1LL + (long long )x1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea0d09c3-347e-4fc6-aaff-b2a825cba6a4
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 24
    column: 9
    function: main
  location_invariant:
    string: -1LL + (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 781a0ff0-e97e-4933-ad80-347ce3a58de3
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 24
    column: 9
    function: main
  location_invariant:
    string: -1LL + (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b8dc010-4749-4517-926a-fbc9806100b9
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 24
    column: 9
    function: main
  location_invariant:
    string: x1 != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18030b6c-9bd1-4d1d-8668-2c35e473edcc
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 24
    column: 9
    function: main
  location_invariant:
    string: x2 != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d78b88c-2e00-4fa2-96ef-1c683b8d3581
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 24
    column: 9
    function: main
  location_invariant:
    string: x3 != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b577558-27f2-4cda-954b-a1484131e8e8
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )x1) + (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b554514-f58d-4b1f-a68b-d900bc198f61
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )x1) + (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d9a111f-cd27-40ab-889f-dd524e3ec94c
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )c2) + (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73a9cb71-d243-4001-8970-06616aff2638
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 25
    column: 4
    function: main
  location_invariant:
    string: ((-2LL + (long long )x1) + (long long )x2) + (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5ca3f79-fd84-4423-84c8-d93c2a5a08ab
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )c2) + (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 265fbc89-34fb-4624-b3db-35999ea28ac3
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 318fad4f-8cf3-422b-b727-a584716cffe5
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )x1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6703bb5f-3fc4-4139-8875-c28f6e7f969f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eaee987f-e15a-493d-a337-2377203f5c07
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )x1) + (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d84fe9dd-449d-4d8f-b63a-7036547a5537
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )x1) + (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93b00a60-f93f-4522-baed-a18403677bab
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )c2) + (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a02e884-86ae-4c59-ac80-9c6c1c677f87
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 26
    column: 4
    function: main
  location_invariant:
    string: ((-2LL + (long long )x1) + (long long )x2) + (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0919ab4a-843b-4e5b-a917-cd2de3be05d3
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )c2) + (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e80c37e-d0e2-4a0e-badf-a18cc3004fbb
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 1LL - (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa485453-c1dc-4f84-b251-61b7a122b258
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ad23e43-4d6e-46fe-820c-77c964ca3fff
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )x1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8696da15-e505-429d-98d4-75a38b4409c7
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab3aacc8-8edb-49b4-b4ad-53e2f1085a02
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f18a0950-586f-4987-a6f9-fdea854cb882
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 29
    column: 2
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fac1dde9-611e-41aa-9e07-068bffe0dcca
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 29
    column: 2
    function: main
  location_invariant:
    string: ((8589934590LL - (long long )x1) - (long long )x2) - (long long )x3 >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 270b47bd-8df1-47e7-a6fb-4cb7a5dbf8d8
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 29
    column: 2
    function: main
  location_invariant:
    string: ((17179869179LL - (long long )x1) - 2LL * (long long )x2) - 2LL * (long
      long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40099cac-cb7e-4482-a13a-108d10de3310
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 29
    column: 2
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b001d520-1d89-4564-be65-a212f1dc1b13
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 29
    column: 2
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13e077f0-bee7-4317-83a6-a8e49012fbc4
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 29
    column: 2
    function: main
  location_invariant:
    string: ((8589934590LL - (long long )x1) - (long long )x2) - (long long )x3 >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d782dc54-5bec-4363-b437-1111bdfe3041
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 29
    column: 2
    function: main
  location_invariant:
    string: ((17179869179LL - 2LL * (long long )x1) - (long long )x2) - 2LL * (long
      long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7cb9b3e-83ba-4886-a3b3-7f64a9284058
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 29
    column: 2
    function: main
  location_invariant:
    string: ((17179869179LL - (long long )x1) - 2LL * (long long )x2) - 2LL * (long
      long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 199d3e77-58b5-4bbc-aa9a-68af6017f0a4
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 29
    column: 2
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 826f1b5c-eea1-4b3d-8ca0-f437c6549fd7
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 30
    column: 2
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec4a7574-90b0-4ece-89ca-dc4a57ab63f3
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 30
    column: 2
    function: main
  location_invariant:
    string: ((8589934590LL - (long long )x1) - (long long )x2) - (long long )x3 >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 089e9c5f-38e7-4784-aab8-e5162cf58713
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 30
    column: 2
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1862bc8-e4fa-4ff9-9162-f2ef36f2df87
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: 1LL - (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d4cf155-598d-4832-8f7f-072f595b5d82
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84610ecf-68bd-4809-9c93-c53dab46cf70
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92a69dac-8ca4-41d7-9a53-445491d13dd9
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: abb722dd-095d-408a-8236-59ca5bef451c
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b76d255-f988-47d8-ab6f-f88c75e4446d
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3edff50b-0ae6-425f-b398-7a710c1b3d8f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2243dc7-a4a6-4efe-b2f3-f5ecdf1e24fe
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9f184d5-4fb0-420a-b509-b23a591ad482
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: (long long )x1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9bb55fd-364e-4e76-bb57-8120abefc684
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e7784ef-ef09-476e-bbc2-428a624e5e6f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41a3240a-5bcd-4146-b95c-7bc6a6ea60fd
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: (long long )d1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98b9908f-3883-4f40-b189-ed9ef1d5b18e
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: (long long )d2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4f072bd-8dfa-44ce-ab37-6c3d9f3cb350
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9a4c19d-7e29-49af-9ca3-f4629a837832
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 803a148e-c5b2-4d88-b06d-a74cb37066c7
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 15
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01fb9994-700d-43bc-b35f-02f03727dbcf
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: 1LL - (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b4e3f5b-ad0a-4550-85f3-47ba6896f335
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44222058-5e37-4d76-822c-7930690ccfef
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 938009a8-4023-4acd-aa96-acfd90861b22
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a0c5593-db0f-4908-84d6-aadf4ee43d1f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cba9866c-2a1e-4b01-a888-f51ad0f59a22
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a66a0d03-5667-4fee-9ccc-888d06ed6a35
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62897e23-87c2-46b3-9636-f8e7e41d6df7
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: (long long )x2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca26c2eb-af1a-4733-b896-a39ccbb5e7b9
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7394bb2c-ff32-4649-a7e4-173231305ec3
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: (long long )d1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad5c4202-d207-4523-b949-b75e891b5116
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: (long long )d2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c1ae550-1a94-4011-9e8a-20fdbf1cf09f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2271f9ef-1718-4055-9449-afa9351f813c
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af572ac0-e7b5-479a-b9b3-3bd89f04b7d4
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 44
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a782477-67e5-40c3-a146-c72a272ab9ed
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: 1LL - (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60c6600a-70cb-4236-aad5-dd0a33fc6a50
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b6d0f26-8760-4b17-bd5a-fd2d19adeeab
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0481da60-704c-4730-ade7-1cae900d6af5
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f29625a-f8bb-43a7-a74e-10402ecd122d
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4263fe9f-0745-48ef-a07d-591a7ff1d559
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3669d349-7757-4cd1-874b-fdf177f787ea
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: (long long )x3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e4a2668-9868-4149-9cb9-82795ef94c49
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: (long long )d1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c96a6093-87a3-4544-b911-81131a1a1bb9
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: (long long )d2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a1dcfeb-98f2-41bf-abb9-fbe91c3c47cd
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 114d5132-1118-4fe0-acab-f780ee14fb02
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ba55ea9-cae3-4872-aa4e-0c1ca583d56c
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 16
    column: 73
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43207151-d99e-446c-b74c-35e97ef95cc8
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 1LL - (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a857c299-d186-4171-aff2-6569d22f620a
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58caa334-dbac-42b9-b26e-c0f2a18e750f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6fe2f26d-158b-409f-89e7-0215e8c8ef49
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 883048ac-5496-4a31-9f8f-71e32ae94e48
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 296cb87a-1cb6-4b7b-b016-e16ec603a98f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )d1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ab7fbb3-b8d9-4498-b192-21d7aa2e32c8
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )d2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2833d339-df65-40f1-8be2-07840c80798b
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e279e53-6396-4fde-8e94-a8a88bfc516f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 755c929c-f30a-4e63-adc1-8233d6170eeb
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 15
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1befd445-fb2b-4213-94a3-a23c34f5ac97
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 21
    function: main
  location_invariant:
    string: 1LL - (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98689684-4557-4cf1-9268-eb7a95dac18e
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 21
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56e7f8db-8882-4019-b4ab-3f0a65514fb5
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 21
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8892664d-0e80-4cd9-834d-26df8496011c
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 21
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f16db3fb-3c29-42ee-884a-99f77c719cd5
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 21
    function: main
  location_invariant:
    string: (long long )d2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e59f202e-b128-4eda-8d82-7c4fec6b911e
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 21
    function: main
  location_invariant:
    string: (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40576692-0b8b-41a8-9311-0d7f69a6e7c3
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 21
    function: main
  location_invariant:
    string: (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 094fba49-2170-4804-bdd8-78ca131aa85d
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 21
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdc14987-c65e-4fcf-8b6b-8aacb7bf88f0
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 27
    function: main
  location_invariant:
    string: 1LL - (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dddc9bd4-f5fc-4526-9ba3-2890d92223f4
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 27
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d78537c-61be-4b70-affe-ab1821b1f867
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 27
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5c44739-9b4c-4647-b254-cb14b771ef83
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 27
    function: main
  location_invariant:
    string: (long long )d3 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1287d3c2-9cbd-438a-b474-761ca7e74ff8
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 27
    function: main
  location_invariant:
    string: (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38ab24e4-d73c-484c-accc-af223dca11c9
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 17
    column: 27
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bf00348-d0c9-495f-a214-85acf020add3
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 18
    column: 8
    function: main
  location_invariant:
    string: 1LL - (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 775ec5d7-19c5-44be-9e40-9609209a17af
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 18
    column: 8
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a948f8e-297c-4258-b9e4-3ab9ea17b03f
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 18
    column: 8
    function: main
  location_invariant:
    string: (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43bf8537-d0d2-4dda-99ac-59babd71027b
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 18
    column: 8
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9d2e467-a843-4edc-a174-36678890bf04
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 18
    column: 37
    function: main
  location_invariant:
    string: 1LL - (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4aba66c0-7183-40ae-9343-c709846fb52d
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 18
    column: 37
    function: main
  location_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5a5b309-e600-4373-b473-f2f0eda7e0e4
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 18
    column: 37
    function: main
  location_invariant:
    string: (long long )c1 >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 244cd4e0-bf83-403e-8418-71c361470588
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 18
    column: 37
    function: main
  location_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c273dd54-2fdc-49ec-857d-47719bacb56e
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 20
    column: 8
    function: main
  loop_invariant:
    string: 1LL - (long long )c2 >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c0c6c116-5c43-43c7-9244-49de53410bb6
    creation_time: 2023-01-27T16:31: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/trex03-2.c'''
    task:
      input_files:
      - ../plain/trex03-2.c
      input_file_hashes:
        ../plain/trex03-2.c: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/trex03-2.c
    file_hash: 1665535fec7adb14e6180ec62b52e4186e8e47f5c3033c1fd0e7c0223e023043
    line: 20
    column: 8
    function: main
  loop_invariant:
    string: (long long )c2 >= 0LL
    type: assertion
    format: C
