- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8bfca33-2fe6-4a07-a8e6-2133e0aad7fc
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba2782e6-54d3-43c3-9bbd-77178089f030
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 35
    column: 8
    function: main
  location_invariant:
    string: (4294967295LL + 2LL * (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 088928e6-6a8b-44e2-a138-9d8cdf88372e
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 35
    column: 8
    function: main
  location_invariant:
    string: (4294967295LL + (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 690b4a35-7060-43f3-9439-f8f4685b0f2e
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 36
    column: 8
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b549205e-a65b-45b7-a8e3-656f67479f00
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 36
    column: 8
    function: main
  location_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1c2dd7c-3696-4ecf-9c62-8231c0879983
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 36
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9dbf8b2f-2195-4761-89da-fc8b44a9e5ac
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 36
    column: 8
    function: main
  location_invariant:
    string: (4294967295LL + 2LL * (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9127735f-9e51-49f6-9b80-ac56df7a675d
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 36
    column: 8
    function: main
  location_invariant:
    string: (4294967295LL + (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3fb197e8-2cb9-41ad-88c6-62539fbaa957
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 37
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27423c34-e578-4805-be86-551bbdd9148b
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 37
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1834f2e-e50c-4885-b8cb-3dddce51ca96
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 37
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70c075f7-f1c3-468f-a61c-b80b432d02bd
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 37
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45aba99c-145f-43fd-b3de-0c7e5a867475
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 37
    column: 8
    function: main
  location_invariant:
    string: (4294967295LL + 2LL * (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0136b07d-92fe-4d51-9ad7-ee9160358f0d
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 37
    column: 8
    function: main
  location_invariant:
    string: (4294967295LL + (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c968a673-21f8-4ee1-a666-b18d2fbe5ccd
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60a1867b-e897-44d7-b0c8-de7bed9cabbd
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e84d0744-bae5-42ef-8447-8fa78bc57152
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c561d94-e10a-4a5c-80cc-c0176161ecef
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 38
    column: 12
    function: main
  location_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87e44688-49fb-4097-af95-0b44be87fdb7
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 38
    column: 12
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a62646e1-6269-4426-8659-61aa76a94cb8
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b74f1cf9-4d1f-4f8d-9da7-4dfb238b92ba
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 38
    column: 12
    function: main
  location_invariant:
    string: (4294967295LL + 2LL * (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f51679a-8693-4114-acb4-d5aa97305984
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 38
    column: 12
    function: main
  location_invariant:
    string: (4294967295LL + (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 247efad4-3fcb-44e0-89d6-9d048bbcc248
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7fd22f1-6a7c-4c78-9dc0-17cd26477fd6
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 40
    column: 8
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 042665ea-7645-4be4-9b20-ea2bf640d4cb
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7208922-483e-43d3-abc9-1abb881ff743
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 40
    column: 8
    function: main
  location_invariant:
    string: (4294967295LL + 2LL * (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0592218-38b4-43c8-bf16-fef094eab5e1
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 40
    column: 8
    function: main
  location_invariant:
    string: (long long )A - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9108efa4-0b4d-4987-96ce-22bc3f9b14ea
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1da4ba5-5f05-4030-a50c-8ce137fff27a
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b2de03f-471e-4f71-8b00-88c67e9fc7de
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 41
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bfd55e7-88ce-4c0f-a1d0-a696979386ae
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c1b84c5-6ea8-45a5-90ef-8bc1eda55643
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 41
    column: 8
    function: main
  location_invariant:
    string: (8589934590LL + 4LL * (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43952852-e0b5-4a1a-80ec-8974ae2e4419
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL * (long long )A - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f35f0a57-48ba-4688-b2e2-ea8b59df8788
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 45
    column: 8
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bce7ccb0-45c8-401b-bd20-1d0d33d34d0e
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 45
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0aa1d632-a425-4c28-9b68-08a7f6c8a44a
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 46
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93ffb266-4594-4dad-a752-e9b658c694db
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 46
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5208ff9d-5338-489c-a585-a69c847673cf
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 46
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e74bf6f3-a075-42de-80ae-d8d42b258998
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 46
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7f364a8-bf0f-4479-8c54-46821aea7cd4
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 48
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dab514dc-2eeb-4024-8c46-50fa9ebcec11
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 48
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 830b6503-2aa5-4b51-ad74-ccb8ff9b39a5
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 50
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a668b6a-6e5b-4c13-be35-2078408f069c
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 50
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3707d99-e8b4-4db7-883f-c20e34d5ed9d
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 50
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 642fc02b-94b0-4484-b583-605e08b86bb4
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 51
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4580a597-392d-4fad-a1df-2c888719c528
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 51
    column: 8
    function: main
  location_invariant:
    string: 2LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9175270e-5a3a-4d01-9b97-f3c93c199ae9
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 51
    column: 8
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c11b0f3-50f9-44c1-a37c-8e0bcd9253db
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 51
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8cada4d3-b9c3-44f8-92f3-01a6b996da0f
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 51
    column: 8
    function: main
  location_invariant:
    string: p != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7e7c3d5-11f3-4a77-ae97-8d896be78fcc
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 51
    column: 8
    function: main
  location_invariant:
    string: p != 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd91f41e-efcf-4baa-80e8-f61a9e4ad0dc
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d6a6e21-af90-43b9-9b7f-7d9a7ee97e99
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d345eaf-9fcc-4755-8bce-06ac968ff7e1
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be4f4ff8-7f0b-49ff-8385-1927bd1d1f69
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 52
    column: 12
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 524c6e1b-9659-4086-8df9-850f28d78f57
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 52
    column: 12
    function: main
  location_invariant:
    string: p <= 4611686018427387903LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 513f0518-7c74-4873-b095-53cc9f450620
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db4c535d-cb21-47db-acce-fc2b7010e0c6
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f52303d-c4a8-4b2d-af46-8479bc961b68
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0aac63e-8557-437f-bb1c-5b5d9b99fc71
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 53
    column: 12
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c8f638f-0913-49e9-bb73-0da73fb0f1cc
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 53
    column: 12
    function: main
  location_invariant:
    string: (0LL - d) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d51241a-5e61-4a7b-8e2d-e709656d9df4
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55e91a6c-2ed5-44c2-a964-6b88339e967c
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 54
    column: 12
    function: main
  location_invariant:
    string: -4294967295LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 288aaf03-fce3-4911-824b-9f6d4de6a509
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22fba113-f2fc-488d-a692-afdadc13709e
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfb7fccc-2ad2-4d3c-a60b-71b6d9786604
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49beee97-25bd-440f-8603-99f69be44397
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 54
    column: 12
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 460c6829-cd98-4985-aaf3-b44acd2c1085
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 54
    column: 12
    function: main
  location_invariant:
    string: p <= 4611686018427387903LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d41d8a3-b43c-4639-81fd-d1e4d47b7bfa
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 54
    column: 12
    function: main
  location_invariant:
    string: r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdce7e58-4e58-4d3d-9942-688007368cb5
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87b4ed51-80f9-4775-a40e-58e12d49d34e
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 58
    column: 4
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 062eb952-c10f-46c0-a89e-dff34a21a6a6
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 58
    column: 4
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73551e50-1c50-4413-a353-a42768068f90
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 58
    column: 4
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d80f1ac-3a3d-40ff-b331-04142753d549
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 58
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 380f5e84-3dbc-48b3-a8ff-dbac4ab88cde
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 59
    column: 4
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9bf58304-c17b-45f6-84e0-07001f7ce7a5
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 59
    column: 4
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d6d9061-dfbf-4d80-8e8b-6a2de8d05a32
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 59
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 200d83a3-5376-485e-bcc4-a8a93ac433e2
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 60
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9b243a0-22b7-4ae0-af0f-055320d12aed
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1d1413d-352e-4de5-a237-0ff906807521
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d018fa8e-5db6-45b5-a27f-244b07123b00
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 149390dd-757d-426b-99cf-d3f30e51cd6d
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fed34476-2ea0-4935-b67e-9f70d68bd68e
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd876172-29d3-4ba5-9ca6-1a902caf34cb
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c162e9a5-ed80-4a86-9d54-bbe93658306a
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56fc1271-0ffe-4fe4-9634-0a9882c780e5
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb16b9ee-d975-4282-893e-bebb9ea033ad
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 676ddc7b-7250-4564-b001-e898b7a43941
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f07a93bd-27bb-4bb6-b6f2-48f2b863a4b8
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d241f072-aa18-4569-ba39-d8f4c6ebb219
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 169d6fec-9717-4399-ac25-90745b3b5658
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e8346e2-59c9-4e15-928f-222b3c1cd082
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f78b3c7-8c36-4d55-aca9-496f4d0f830c
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3281e2d1-9b7c-43a9-bbf0-efded7737146
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9c8f567-a466-4d68-97ce-d5391ff81e84
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f1b6d72-2f71-44fa-a2fe-d36670302831
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 30
    column: 4
    function: main
  location_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc15777c-ac6d-48db-99cc-2121a857f740
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 446f46f5-5cbc-4868-8898-87c12dc35ae9
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33f0ef08-eb03-4443-be8e-1eea60ee918e
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b8744d2-a89d-477e-b98e-c5a6a9539490
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47884159-730e-46db-98dd-3e6695c1e238
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3821015c-b384-4d01-8155-016c5a0fc0c8
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 31
    column: 4
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45b47ef9-6f40-4f98-9a3b-9017093ee52a
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87b91105-fc7c-4138-a506-06d4e596603a
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 896a9c03-8c6c-45bc-bfdb-f320669256a7
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 725799e4-2bab-4735-8f77-73b5adbdbc2d
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06ac64bf-b7b2-4844-b872-e24f4e6f8dc6
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c64ed3b0-cd6e-4133-9680-a627fd58699b
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0638042e-113b-4d65-b708-c859695360f2
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 101b5b91-a415-4761-8f8a-9b2167f46374
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dec1b852-133a-4b65-af1a-32678547a1f6
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b2f81c4-caa7-44bb-bf09-eaa50c359de6
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e84ee648-5fe9-42c0-990c-b4b8ccf12d17
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d47a78b4-be13-4445-8b09-ff4689e42528
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f7547f13-3481-4358-a217-4138ee5ed5a3
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f85c9429-a7c7-4d34-9780-0983f02d770e
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d8cbd3d5-ed63-4b84-aa8a-ad23c8ef10b3
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: (4294967295LL + 2LL * (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b5a2ee4e-e733-4e1c-9d3d-8a0c58592dd3
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: (4294967295LL + (long long )A) - d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6135ed90-1c55-4680-b9df-8fe0090d2368
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 344f3104-8cb3-4c32-abc7-db997252bd7b
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 29431f91-f994-4e79-a3be-1c8c7e359d62
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b4658057-70ce-4e9b-8cc1-f99e055139e7
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 103eb5ae-967b-4079-abf7-4d3f97e2abae
    creation_time: 2023-01-27T16:29:35Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll.c'''
    task:
      input_files:
      - ../plain/hard-ll.c
      input_file_hashes:
        ../plain/hard-ll.c: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll.c
    file_hash: 8c31bebbbf1ab8c6e57b91fec88eba145fb9c1b52fce25f48cae26620a3d8ba6
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
