- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0f827ce-a8e2-4bc2-acc8-fbdcbb8efec4
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 34
    column: 12
    function: main
  location_invariant:
    string: -9223372036854775806LL <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40878c90-9fbb-478e-ad40-cecf4ad3bf61
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 34
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 729ee6ee-3959-4331-b230-ef701e514fc6
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 34
    column: 12
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f92d84f-745a-4dde-8a22-e884a9f85844
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 37
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775805LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b96aa88f-eef4-47a0-8c08-4438d99a943d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 37
    column: 8
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: afbfc7d5-22d8-4827-9547-c536c253c70f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 37
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad943be7-c8c4-485a-aad2-884fe811598c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 38
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775805LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2dbe5de8-4370-4ce7-bc6a-95d790e6b16a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 38
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c5d3c39-5bf0-41bc-989b-fae4e4911c6f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 38
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1970dfb-bf60-4259-b567-b86505a3b212
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 41
    column: 16
    function: main
  location_invariant:
    string: -9223372036854775806LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 853ada37-d0c6-41bf-bdd0-b54afa708ad1
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 41
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83364f72-68aa-43a9-b5eb-d3e902542687
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 41
    column: 16
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1097de40-34f7-4c7f-9609-932a1d5c024a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 41
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf2a992c-f8b6-4f10-bf74-5f5b89e63057
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 41
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 30fdaff5-d196-4014-ac7e-d84a45f32829
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 41
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0d98835-8602-4da1-bec8-a48a40530443
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 41
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56d21c56-5db2-4d64-b717-8ce692091c0a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 44
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39667c76-ff13-4dc1-9e3a-3306d4e5408f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 44
    column: 12
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4945cafe-da4e-4a39-899f-8c5c9a79e287
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 44
    column: 12
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97a7d8e8-8589-48dc-9893-b1f258f161f8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 44
    column: 12
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3eee712-bd10-4638-b639-4f93837bee57
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 45
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af6370f7-a94f-42d6-9a56-b8fcc2151b12
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 45
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d7919c1-3ac7-4809-8349-86441ae01f1a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 45
    column: 12
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2aa1a17f-9a73-48ea-b308-a700588f221e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 45
    column: 12
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fcb99f7c-3d81-4a0d-894f-ae9228738df1
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 45
    column: 12
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b85e38c-796f-41ea-9503-6238d9a41c82
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 45
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39d24f1e-75ea-45d0-a485-b5c679a294c6
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 48
    column: 16
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 422a65ff-c022-4776-a9c1-dbcce9c116cd
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 48
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f781015-792d-4d8f-9675-fa131d6c9ca9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 48
    column: 16
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 635f4025-7cf0-45bc-9239-0034a320fcdf
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 48
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1c55af8-3f29-4f4c-b3d1-3204a89f0e21
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 48
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 74e03b0c-42f4-46af-87b2-be6c87dd1b31
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 48
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7e5f727-7c9f-4df9-80cb-a2bd48cbca8b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 48
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31405f1f-652c-4907-9a0a-a9b7dbbbdc03
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 49
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 456e7aba-1284-4308-9082-d493cd893c3b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 49
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 836386d4-9cc1-432e-9fcb-9e516273c994
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 49
    column: 16
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f65a645-3fca-49d8-b443-8b87aad7182a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 49
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4af38980-5526-4fce-bbc7-a9882c61ef4d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 49
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d5b52bb-a61a-4189-a73d-7bcab564be15
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 49
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec03474c-b98c-4ba3-b0da-262427153885
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 49
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b637874-ea6a-416f-954c-842c25f591ad
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 49
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1101497a-a3af-4029-866e-f43c733e5c83
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 50
    column: 16
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3175b016-a79a-4df1-81f1-884fcb6892db
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 50
    column: 16
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e30f1f83-6f29-4379-9f21-c98c10755db8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 50
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 158e8280-c07e-4bc5-8bb0-c33619379ab9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 50
    column: 16
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16841ea7-16cb-4d4c-9c3b-613fa8b04a62
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 50
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3e82838-003a-4695-b1b5-09b0aef7edb9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 50
    column: 16
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a512f36a-4013-473c-85e7-3ac418cc479d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 50
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c7637c0-cad6-48e9-896e-447c1eea4b19
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 50
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe361786-b639-411d-baad-a450d72d3126
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 50
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ebcde5e-470f-403b-8b9b-a5fdd7d8659e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 50
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec1c1592-6e89-430c-9363-4f806056c255
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 50
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69634c45-8cd8-4162-ad6e-2ebb2848f931
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 51
    column: 16
    function: main
  location_invariant:
    string: 1LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 222f1ab5-b98d-495b-9832-9c95b2a363f4
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 51
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2aad8426-e660-4436-88ec-9f767fb9dad6
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 51
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6aa70e8b-f795-4946-bc67-fd55c6dbe090
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 51
    column: 16
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40aa3707-d3a9-4ea0-bc82-70734356593a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 51
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28870217-1d4f-4d1f-b424-93b711476d1a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 51
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a68f0ca-a35f-4183-b773-132687fa05c6
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 51
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95a8dcf6-f9f0-43a2-b228-d2d35086d7cb
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 51
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 542ba8c8-63be-4c26-8f93-0593c3cda3a5
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 51
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 289360b8-ee1d-47c9-8592-3b423fd6b564
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 53
    column: 20
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dfaddfd3-18c1-4e0c-9136-f926e3c64b99
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 53
    column: 20
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c59d2885-13db-4e8b-ba8b-7dc74cdb9f43
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 53
    column: 20
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9449da0b-227e-4a21-b9d6-fb1026b7937b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 53
    column: 20
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c7332c1-8e3d-4828-bce6-9015a88bb027
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 53
    column: 20
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50733eeb-223e-4420-89cb-bb8459e18a54
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 53
    column: 20
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f84f0a40-660a-4f76-8371-8e47d6918379
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 53
    column: 20
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3ebb7f0-ca2e-44d8-a33c-54be474090fd
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 55
    column: 16
    function: main
  location_invariant:
    string: 1LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad01449f-4188-4c1d-9587-eebb1278cc12
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 55
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23ecc883-43cb-4dc6-ad4a-50e42682e5f1
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 55
    column: 16
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dca633fa-d6f0-49e2-8721-43aaa95eb64d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 55
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0ba680b-625c-42b6-b9b5-79620a9228be
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 55
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e0278bc-68cb-4e44-a19c-039854558a6f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 55
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b17db7d-ff92-4e86-9e56-aca2892f478b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 55
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 284761c3-23c2-4bdc-9617-8421ada5518e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 55
    column: 16
    function: main
  location_invariant:
    string: c - 2LL * v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee85bb00-7b06-49b9-8a29-5cd0f2db8c4e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 56
    column: 16
    function: main
  location_invariant:
    string: 2LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a6525cd-c971-491e-b3a2-ac787b242dfe
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 56
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 969d6817-2173-4082-b5d3-ea0d8c0bfd83
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 56
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1caa4e40-cda6-4e85-82a5-1ff4e3433452
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 56
    column: 16
    function: main
  location_invariant:
    string: -2LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 477129ec-5863-4994-8486-81356924649c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 56
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7277f5ad-8a2c-4093-896e-12c53e06149f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 56
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f3537dc-5cac-43e1-909c-4973d3ba8740
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 56
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c09f33c-c781-4a77-b27f-eb85ac3ea439
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 56
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78006f49-0634-426b-b1bd-762028409ffb
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 56
    column: 16
    function: main
  location_invariant:
    string: c - 2LL * v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a9b1f86-a9e1-46c9-ad23-53422f4f376f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 56
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65993d15-95eb-4dc3-9f70-e7d233277df7
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 58
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56227476-f2fb-4269-8ab4-885861ee4f8d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 58
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a04b200-ffa8-41e3-97fe-584f186ea7d1
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 58
    column: 12
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16dea27b-2a66-4ed4-809a-6c770bf76830
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 58
    column: 12
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4e309bf-cd15-4dcd-94ab-5355a1ba467a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 58
    column: 12
    function: main
  location_invariant:
    string: (-1LL - c) + 2LL * v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed6c1a32-f482-421c-8b30-63ff8c77abcb
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 58
    column: 12
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5e66512-246a-48ac-b603-fe9fafedd3d2
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 58
    column: 12
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b02c5f23-7f20-485f-b38f-45cf8743e8a1
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 58
    column: 12
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9968373-cb33-4e6e-a47e-947dab970d52
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 59
    column: 12
    function: main
  location_invariant:
    string: -9223372036854775806LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ed22056-e4d6-44ee-8fe7-dcf5c2ac1107
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 59
    column: 12
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6cba239-8deb-449e-9af1-680fdba28910
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 59
    column: 12
    function: main
  location_invariant:
    string: 1LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af135af0-0106-4bfe-9264-6aef638a5f84
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 59
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07ee7b1c-d961-437e-a2d8-f2ee64ecef3c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 59
    column: 12
    function: main
  location_invariant:
    string: c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ed765c8-2b08-440b-8f7e-79b0a7b37759
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 59
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef7fcb1d-c1e9-4a47-8e66-a0df898bf2db
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 59
    column: 12
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c03533c7-9f36-4a1d-8990-2a308997473d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 59
    column: 12
    function: main
  location_invariant:
    string: ((0LL - b) + c) + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f47302f1-bf25-4652-a0bd-4e837ee0b5a6
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 59
    column: 12
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ef790cd-37c4-49a7-8205-04951458b336
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 59
    column: 12
    function: main
  location_invariant:
    string: (-1LL - c) + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08b1fe46-6d9c-4762-b668-a7536036e806
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 59
    column: 12
    function: main
  location_invariant:
    string: (a - c) - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ed30182-a299-4044-88aa-9c822911c4f9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 62
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775805LL <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 772b163b-64a2-4b06-baa9-c63b294df990
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 62
    column: 8
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c9a7bdf3-c21e-465a-8491-9f226bcdc399
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 62
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f65023e9-7508-40e8-a824-903a21d9cb02
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 62
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c594264b-d0f2-483c-bc10-b7a26af07c51
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 62
    column: 8
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca0da4e2-dc06-4552-b7eb-150a105bd1b9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 62
    column: 8
    function: main
  location_invariant:
    string: (-1LL + b) - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d486e0a6-94eb-47c2-8f08-3a0b34287c05
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 62
    column: 8
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 842f1049-cb4c-4b54-84f4-cc35325e8c66
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 63
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775806LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e70476c3-67e3-4935-b680-6dde0f80c411
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 63
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775805LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e79053b7-88e7-478f-827b-0c6f39e8e757
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 63
    column: 8
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3b37e1a-02c3-46c4-8f38-9a9b70ed8271
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 63
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c25d84c-b03d-4022-8d87-a3e21427df09
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 63
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50e541fa-ea82-42c1-823d-b2f4318708c5
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 63
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - c) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4cade97c-f22e-4ba1-bf5c-ec805f9a0fcc
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 63
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6db739d0-7a7e-4ebf-b28c-7362a146b312
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 63
    column: 8
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ea69e2e-6146-42d9-8498-9e43e6fcd58a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 65
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775806LL <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c465bbc3-9085-4363-bded-d8dd48f5622a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 65
    column: 8
    function: main
  location_invariant:
    string: b <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 61f8e5b1-b9c3-4911-bfb9-7738bbcb481a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 65
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 753948a4-b08e-4850-97df-4fea6f108798
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 65
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00ca1113-15cd-42aa-b172-9c786c6c4271
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 65
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f25c7421-4021-455e-80f6-8a28c65b53f9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 66
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fc67ea7-a861-43f1-b199-e06a098ce057
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 66
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9af9618-16f9-4be7-b117-294f0200b752
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 66
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b00f5b54-e368-4771-9cf7-75f5eafe4180
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 67
    column: 8
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0c73cd6-2b77-4b62-b80d-7be13eea033c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 67
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0250d7cf-4490-40b9-a5a1-401a14e3337f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 67
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da17b131-beba-48fc-b9d8-bfb2dc87fd50
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 67
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c5f1971-5704-4324-b196-3ab7e2d5cc33
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 68
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b50e896-695a-4d26-8bcf-7022d3f48f1c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 68
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 248c7568-c0e9-46af-bec2-b86567868c83
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 68
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 424a79aa-dc09-4d88-9d9e-13d379e73bb0
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 69
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec98a53d-90f8-422d-813b-1bf0679c750d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 69
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb45eb98-c012-401a-8a58-9b62e24ba934
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 69
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd00b139-7512-4970-846f-2d66983a6d35
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 70
    column: 8
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b430092-3351-4a15-8961-d00bba6f6653
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 70
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ce48fe7-b7ec-4de6-afcd-64ac01a37ca3
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 70
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 90d37311-8f09-4e55-927e-4a99b2f6f4f8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 70
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fc8ad29-5760-481d-bc69-b8d717a3edb8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 72
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775805LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f6c5a33-9def-46d4-8156-4dbd3a712316
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 72
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f384724d-6a0b-425c-8444-83ae422200b5
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 72
    column: 4
    function: main
  location_invariant:
    string: ((0LL - a) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aac178ee-03ea-4f42-a9f6-097ec856973d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 73
    column: 4
    function: main
  location_invariant:
    string: ((0LL - a) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa9dd508-c199-426d-bb56-00bc474cdbb1
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f3c5dcc-636c-423e-8fca-2437e6e6fabf
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 27
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a63e3f9f-88c0-4648-82af-fb884b047d4c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4b967a4-e16c-4ea5-ab0c-1d37ef873570
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 28
    column: 4
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a59f17a-b8c3-4b5e-8bcb-db79fef21296
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775806LL <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e991d93-7965-4bdf-bfd1-4ef2f7acfa6b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775805LL <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e1180c0-2cdf-4f64-a43f-e4ed08f7a840
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e7794d94-93bd-49cf-8fcc-240de2c7369f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f2c92c6-db2e-4b73-98df-0dece96cbd61
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 60d19f00-2473-4c02-9226-f0554f3f52a4
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 40
    column: 15
    function: main
  loop_invariant:
    string: -9223372036854775806LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d931ed83-5ddb-46d0-b4ae-cdcd9332f93b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 40
    column: 15
    function: main
  loop_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b433545f-5ab7-4e03-b6d0-6580199bbca9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 40
    column: 15
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 49a86bf3-74ec-4ff9-aff6-039025cbe1c8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 40
    column: 15
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c7fdf7b-020e-40dd-9c42-b94f1829822e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 40
    column: 15
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: df580512-0eff-4f76-96e8-4ba4ce95265a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 40
    column: 15
    function: main
  loop_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 56bbe6df-8963-4d5b-88ef-4e6324e367e5
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 40
    column: 15
    function: main
  loop_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a23d3367-ab52-4743-962f-2ab2a67ab5ff
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 40
    column: 15
    function: main
  loop_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 294d7f83-6033-43d5-9399-9bfdd85c3d5a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 40
    column: 15
    function: main
  loop_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: af239ae1-3b29-4fbb-9f41-1106d9cbc8c4
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 58f5c01f-5b0e-4bfa-98e1-1bd42c26f279
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: 1LL <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: faff94fd-7c78-431d-9234-efb7378bf772
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ea8bcede-18c2-4ba9-b238-313583815960
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 241912ea-97ea-4d7f-ad7b-b8e048c57050
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 00a8ac1d-c26b-4c71-a257-3772bf66e1a1
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 98d91a2a-26a8-4db4-bb7e-e2fb593a9007
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c1d6e65-03c0-4c9c-b143-5ab0b0b10087
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 463505bb-89f8-4f5c-9b6c-c77f58d22a1d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a4b0de66-3721-4826-b148-ec62dfabf182
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 80ad61be-7945-40c6-a131-866e54150ea3
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 297461ee-e3d5-46d1-8b03-7d8230034684
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll.c'''
    task:
      input_files:
      - ../plain/egcd3-ll.c
      input_file_hashes:
        ../plain/egcd3-ll.c: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll.c
    file_hash: 4ef08007570a64191e0df13d14d3e8d62a8022f43f46779ea6f6701a621376be
    line: 47
    column: 19
    function: main
  loop_invariant:
    string: b != 0LL
    type: assertion
    format: C
