- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a75b70a-92f0-4445-a9a5-7dbe33704ca1
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    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: 6076708b-8812-4f3c-b9dc-628ceebd01ed
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    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: 35e810bc-eb0b-45d2-b71c-0dbb2e801926
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    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: e36736eb-88a5-4022-966f-5b8c55fd34ae
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    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: 24b2c89f-4781-4e43-8f01-0ef3e3b3fb4d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: acd48174-a85d-4a53-8d89-3582cf084ab0
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 32
    column: 4
    function: main
  location_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50e31327-2f60-45b6-a68c-a2b5f4f0e9c1
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2b1772c-8851-427b-858b-9ffa53cf137e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 33
    column: 4
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d9aeb37-ead4-4240-ab32-a2ddeb4d05c3
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 37
    column: 8
    function: main
  location_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: afbbc5ac-e5e8-4f63-bf6f-ede21593daf7
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 37
    column: 8
    function: main
  location_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d1317fd-c444-4e27-8ae5-36a521239d24
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 37
    column: 8
    function: main
  location_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0dc3f9c4-6672-49c5-b34d-db12bda5c470
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 37
    column: 8
    function: main
  location_invariant:
    string: (2LL * (long long )A + (long long )B) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c32654dc-6b26-4747-9e0b-c33e7b60b7e1
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 38
    column: 8
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12aa4ca8-9d83-4df5-99a4-5e1cba1ffb79
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 38
    column: 8
    function: main
  location_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4e5fe00-2391-4a60-a959-30cd879f059a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 38
    column: 8
    function: main
  location_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26754b47-0347-44f0-bee6-f64d53a1c563
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 38
    column: 8
    function: main
  location_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 88cc44ae-bb74-4f52-8b4e-7ab3b43ff1d1
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 38
    column: 8
    function: main
  location_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9075942-f259-4669-90f3-146942cc037f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 38
    column: 8
    function: main
  location_invariant:
    string: (2LL * (long long )A + (long long )B) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b222a000-afa5-4255-acf7-c5455f924bf9
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d07b4f50-9421-4cfd-b9cf-25d290ac1e7d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a83503af-cbe7-427c-9a92-7e416fc3947f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 39
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cad6508-3a90-4869-9ee8-7d99081ace77
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 39
    column: 8
    function: main
  location_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e226cf58-33b7-488a-b309-50670b208b25
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 39
    column: 8
    function: main
  location_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4f85ac8-737f-478a-a5fd-1c926e750b24
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 39
    column: 8
    function: main
  location_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09292e60-c023-4ff9-bc53-0456b1e52cd9
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 39
    column: 8
    function: main
  location_invariant:
    string: (2LL * (long long )A + (long long )B) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40df27dd-9ee0-4fc4-a5ed-51d757c5eb2a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49f2edf5-384a-439e-b1b2-ded0e51f1fd3
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b4ca7dd-68da-4d5f-a488-0a099dbd7bda
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf7f3f23-1929-4fb9-b826-ccec4b1c838a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 354808c5-a700-490b-a46b-45e05cafef67
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e59f7f57-bd4f-4541-b890-49d8e4b0702e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e30ed3f6-aa0f-434e-8a31-5f1d5d1558d7
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26d8604d-2c7e-4b5b-b121-c830bbf8ab5d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0dfa6777-7f5e-4270-a172-2ac9932a8dc2
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 40
    column: 12
    function: main
  location_invariant:
    string: (2LL * (long long )A + (long long )B) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22d37b92-f3be-43bb-8416-46469541f66f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0b32fb4-082c-40ac-85fb-04501c2b1c36
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 42
    column: 8
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4747c6af-3e60-482d-8aab-a104e80eba0f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 42
    column: 8
    function: main
  location_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c82076df-471d-437c-945d-ee25177f2830
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 42
    column: 8
    function: main
  location_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9723cff1-403b-409a-9fb4-8866be859595
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 42
    column: 8
    function: main
  location_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4cdd4539-1391-401c-8ba6-2a59be46571e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 42
    column: 8
    function: main
  location_invariant:
    string: (long long )A - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca0a2ee3-7a7c-4cab-985e-04a173f53ffd
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df0fcce5-707f-4911-8899-757fe0b5b74a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0845522e-f2d5-4ffa-926f-bf4308b755bf
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 43
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1e70c18-4df4-4d22-a469-e5b018e7db74
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 43
    column: 8
    function: main
  location_invariant:
    string: (0LL - 2LL * (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 352a1615-a32d-4f51-91b3-657048b30581
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 43
    column: 8
    function: main
  location_invariant:
    string: ((-17179869180LL + 8LL * (long long )B) - 3LL * d) + 17179869180LL * p
      >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c86895d7-d004-4af2-a429-d7763b6c4a2e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 43
    column: 8
    function: main
  location_invariant:
    string: ((-8589934590LL + 2LL * (long long )B) - d) + 8589934590LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9d15b86-135a-4591-b176-81007b2faba9
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 2LL * (long long )A - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8844a68a-4e2c-4f0d-b41c-212581842ef0
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 47
    column: 8
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 786b29ce-8c6f-40a4-944f-c423873e7a38
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 48
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dee205ca-2848-4dad-ad01-7d9f276b46ae
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 48
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3252cb5e-3da7-402e-9a49-58a071acca66
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 48
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d58bd9bd-e311-467e-822f-099b9dcca338
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 50
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 163e5fea-42db-479b-8dac-cf035737aac5
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 52
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9eec6b9-367c-417d-81be-eb6024d87440
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 52
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25d86e96-b81d-4bfe-a5f5-546268abf5fb
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 53
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af627bf0-8533-4023-aedc-ad2c4a30a7a8
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 53
    column: 8
    function: main
  location_invariant:
    string: 2LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 221796f4-22d0-423e-8567-7ea584c4f79f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 53
    column: 8
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0383b59-9f33-4546-875a-938faa384f47
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 53
    column: 8
    function: main
  location_invariant:
    string: p != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b7df2b3-8c8b-4001-bb5f-fccc2d543047
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 53
    column: 8
    function: main
  location_invariant:
    string: p != 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28310c87-7b36-4c67-9686-40b3452ad55c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a23c1e9-00b7-4051-88ba-9a901dc0b616
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b4e8ffd-9f22-4013-9acf-8be14d5a02b1
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7934f0d8-faa7-4373-b452-d9bf044b5cbd
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fddd9ea9-7b16-4ff6-a34b-034bb1ca3370
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: p <= 4611686018427387903LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b3608e4-b36e-4b30-924b-776b83d4466e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 55
    column: 12
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c1f08c3-e929-4673-b171-8be2eeeb9e41
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 55
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75bfb82a-a9f4-4e1d-bfdd-647b04cb4cc6
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 55
    column: 12
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da2d4218-715f-4939-8507-a1be5350cced
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 55
    column: 12
    function: main
  location_invariant:
    string: (0LL - d) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cde94acc-d323-4b1d-ab55-3b10fd11144c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 56
    column: 12
    function: main
  location_invariant:
    string: -4294967295LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b3a03b8-6a2a-4ac5-9bda-12cd795784f8
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 56
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70a1278c-b13e-4c50-813a-afd590a13ae0
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 56
    column: 12
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8391d04d-20bf-4718-8ea4-c4038f4b9f05
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 56
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c68f7d72-5fdb-4348-a978-80142bbf7bb5
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 56
    column: 12
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7fac6a3-28ea-4781-aec3-38db0bec1d11
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 56
    column: 12
    function: main
  location_invariant:
    string: p <= 4611686018427387903LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bdcb3873-6561-4bb3-be1f-275e0606426d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 56
    column: 12
    function: main
  location_invariant:
    string: r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f82948c-ee71-4bf1-bcb5-a1285ee719e8
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 60
    column: 4
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3176c30-8b51-44f7-bd22-ca36299b60d2
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 60
    column: 4
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b69fcab0-3ac5-424f-97fd-2389a88f5a55
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 60
    column: 4
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6733daca-00dd-4aad-9966-7ceacbd0f218
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 61
    column: 4
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e9f2588-ceea-47ab-b37d-259ec04ade57
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 61
    column: 4
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a04b646a-3663-483b-9640-7473997eeefe
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    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: a90e55a9-33d3-4bdc-9d28-21bb4643603e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    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: ab793739-382b-474f-832f-1611b215c62e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    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: 3e620d31-ffa5-4c0c-9cb3-455028e3005e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    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: 3350e907-5cc4-4b60-99c4-15887268ecdc
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    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: 94e491ac-0487-4134-96ee-1109842bea2d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    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: e6d90c21-3ad6-4959-a5ec-04789e5b8181
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    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: d216d6d3-99a6-4f92-b956-9d0f52bc3019
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1adec354-b4fc-457d-9e35-4fe7d7a55f07
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c620d1d-63ea-46d2-8665-22067f164a41
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 25fd8fb6-1ed4-4db9-bed9-e9fa84604eca
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a3289612-1bf5-46dc-8744-fbb387900383
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 963ccd9a-0de0-4bf3-a662-f7fe3248f0dc
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 23fb1c0c-4f01-4f21-82c9-bc9b08b3e280
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 607be041-dd69-4656-a267-42ce5d320536
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8057212e-bed1-4989-a027-0057d88a025c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dd25ced9-0117-45f5-930c-e6c95d15f2b2
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: (2LL * (long long )A + (long long )B) - d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 44a4edc8-626c-485d-9b07-fa55e3563509
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dc996b62-d673-4028-9564-7d0fb5b3214c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ebb1879-af19-417e-bd84-5015a162ee0f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1de3fc7e-deca-4912-bc43-8c6fe658119f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound100.c
      input_file_hashes:
        ../plain/hard-ll_valuebound100.c: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound100.c
    file_hash: e3523bc8254ad35e64aad06fd6e3c84672a9aa19521e18482795d6584edb45d0
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
