- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3e5b117-1498-4cf4-adf1-27024f59454e
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    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: a88ee818-99ce-448b-845c-84a4ad851207
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19a5918e-630a-4baf-8778-318863fe8fce
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0d25b51-4807-46da-87a1-0bd556b428af
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee4270a7-86a7-4dd6-841a-27274a58e4c5
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7fb7302d-a0fb-4398-9478-f7530be754f3
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    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: 49527a17-4e64-4ddf-be27-f7a205e56523
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a55e4f8b-8465-4ae2-95be-9910e5c642fa
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e813a7c-440c-402a-a21c-d1084c077466
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48ee432a-7186-41d6-b295-fd7512bb2809
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21f15dbd-c328-4044-ab28-87711a87c804
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 28
    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: 8eabc988-cbc8-400f-9192-23b3c750ac59
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe818b5b-eb48-46a0-81aa-e89ed57caa0c
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 78c86f28-c259-4437-91fd-96632298a3b3
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 30cd5dd8-c941-4c55-b7e6-17fa72853efb
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ca95bf9-74eb-4afe-b58b-ad02e0555cd8
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 28
    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: a5c0585d-9159-444f-a53c-20a1336ecc0d
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21571197-f92d-4648-bff3-bfaf970819eb
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 55b85c8c-06f1-4e43-8baa-e2a48faffacf
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 378e70dc-0c7c-4b63-97de-2a44499ed588
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9a15862-3ee4-4aa7-af5f-3fd1f8d21d7c
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77ec0b11-6d84-4a4a-969d-7277a634c4e4
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee839c2d-8c21-4c64-a523-7d060471488d
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b88fb561-425a-4c37-b8a4-16ccc83c66a4
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8eb39e87-7ab6-44cb-8003-88bacc7a5743
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 369ddcfd-57b2-4c2a-82f3-935051b08144
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2632dfe5-1644-4946-80ca-91ad3f9521d1
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c53c06ce-7d65-4b6e-8fa9-a4efd0e04bb4
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe3bfe7a-7dca-4884-9b7f-e108bb8524ef
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9545d853-96a6-43a7-b8ec-3ce833c6af98
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d32af67-c01a-46ef-bb58-e1144d268855
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4de51c9d-dbc0-46ad-abb7-f1feeb666fcd
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed30582a-9f63-4c26-9fb4-b6ba70c67724
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 085542e8-c827-4d44-b0a1-e27ead15475e
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd431475-7e58-40a5-8021-e15a481e765f
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfa23e2a-c08e-451e-849a-2e47b9b73a77
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2359880-8a61-4e92-b8b3-ae41aa91a491
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b687dd2e-fc60-43e3-97a5-525ef78631bd
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 440a64b8-aebd-4493-8c48-080685970a25
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e608086-d20c-4071-9948-095a5c68b89c
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4a3344f-daba-4e30-b86b-959e55a716e1
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b92733b-6359-4d1c-b119-7038e754e50e
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 925ca778-1159-4a38-ba42-538a9f15ab77
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85c2caea-2641-4b57-93b0-179c1619da1b
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44124f3a-d38b-4914-9550-a0f3f51d4de3
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 026939e3-ded8-4a2b-80f4-edc39027cabb
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 643ff414-64c3-466b-9274-e981244dcbcc
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11177292-1cd5-4dc9-9616-085dc301f378
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e9693c9-5808-4c60-a1b7-ab8439dab25c
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 42
    column: 8
    function: main
  location_invariant:
    string: (long long )A - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd81532f-7188-4c7f-876f-497035afb03b
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 53
    column: 8
    function: main
  location_invariant:
    string: d <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 557c89ca-e45b-49b7-821b-9560ac089792
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 53
    column: 8
    function: main
  location_invariant:
    string: p != 1U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3987284a-43f4-460f-a34a-6eba4995cd71
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 54
    column: 12
    function: main
  location_invariant:
    string: d <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce4da099-a24d-4e18-b87d-33935b3e6933
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 54
    column: 12
    function: main
  location_invariant:
    string: p <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6929d98e-28cb-46b7-a85e-2852b61d0a3b
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 55
    column: 12
    function: main
  location_invariant:
    string: d <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 813b9285-bdd4-4427-9f09-20f3cdc44b55
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 55
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )d) + (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 026f712b-55df-424d-92c1-28766567c218
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 56
    column: 12
    function: main
  location_invariant:
    string: d <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6a4774b-5b62-40f5-aad8-498dacbc3768
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 56
    column: 12
    function: main
  location_invariant:
    string: p <= 2147483647U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0bd2c750-ebeb-47ac-a9b7-dda16ebb7c16
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    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: d4887352-6a75-485b-94b9-555c40358fd4
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    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: ebc99638-82e1-46fe-98df-764298020013
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebbc44b2-ac1a-4301-9c2d-1ea03ecfb009
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92d16ce0-53cd-4ae1-a570-74ae6d310cf8
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f39fcbf7-e76b-4a69-b3a5-d09d22df691e
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fab5d591-7415-4254-9068-1f36131c0aa2
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    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: f83fa069-b13e-46f5-b0c8-9db76f73717b
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    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: 2910987a-876b-4f60-968b-01eaad3b89ed
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1282b125-1224-4cf6-856d-437f92856b57
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57ae7ad5-2ccf-4fc0-b52c-177c1d31d6d5
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26ca024e-8bb7-4baf-a49f-490e148c0439
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ca73150-204b-41e2-b62d-6b9da854bce7
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    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: f06b551b-c281-485b-9e91-b53661a0c182
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    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: 68386bd4-bcb2-4b89-8bb4-8918cad0a7b7
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16bf52f7-d57e-4018-8183-989adb74848a
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4df73d41-96e6-4845-83d2-9f5a4ff6ea3b
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc8b3ca6-3e18-49aa-8bf3-d6e7b2651db6
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )q >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec7846a6-5870-453d-91e9-e8919dde0124
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    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: e9f7b95d-f3c0-4486-ae4d-83413ff1cf4e
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    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: c9046593-4a8f-40c8-802a-f6f2460f8121
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef65b9e8-eb21-40d1-b502-968da0c979b1
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c154c3a0-82f5-43fe-9d35-3055e62b6088
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1de3200c-ac87-4d9f-8f6c-832a9c2b929a
    creation_time: 2023-01-27T16:29:34Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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-u_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard-u_valuebound2.c
      input_file_hashes:
        ../plain/hard-u_valuebound2.c: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-u_valuebound2.c
    file_hash: 3969c56ba3ed63965cbeb782ee88e7216b6985c490408396983bf5f457467675
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )q >= 0LL
    type: assertion
    format: C
