- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51025444-bedf-4d63-a56c-0db7069ecd56
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 3e6f2801-d742-4509-9417-5579e74d35d6
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 43408fe0-394d-4e12-ad18-a1ad60946de2
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: e1928a9c-2d44-45fa-bc26-7114dd118b0a
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: f5903ce0-2ea8-4b58-8319-09bef90c5cfc
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 915ab6e2-0746-45d6-992d-9753b1638807
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: ad91ab3c-c4be-4c94-be56-a312f0f2a755
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 0a79405c-5fb6-4e9a-874c-32581f451fe3
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: b419743d-9697-4ddf-802a-2690e3efda3d
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 88c02bac-31a3-42e0-ae3a-b46b975aceab
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 1792b904-f031-447d-a940-67ca19357023
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: b4fed1e3-1896-4c53-9a74-537c34352408
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: b6765bb0-68ee-463f-91db-13043ef14ac6
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: ea957901-b38d-4b60-8c77-5743adc6c601
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 0d76904a-47b8-4e21-8abd-08f4073814ee
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: c5ce837d-efd3-4005-954b-ac8134c1ad93
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 6c06dc0f-9aff-47de-8d1d-c9c9f1ca4a21
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 1db51ed6-c290-4c6e-8b6f-396f6446348a
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 3081b809-d611-4049-8eb5-2092fa580521
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: fadf9425-2c11-4ee0-bbdd-b3e95a4720eb
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 50c2eeb2-a733-4e41-8d82-6c885463d0b3
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 2a80b7e3-beb5-4fe6-9a2f-3be264e10058
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 6092aa51-1f72-4f6d-920e-534052fe08fa
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: f897c3d0-1d0d-480d-9d9e-a47aad2ac52a
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 1e20994c-3446-406f-9c4d-698d62e75afc
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 0597873f-274d-4049-98e9-19d5e5eb0549
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: e0b991b5-b1c2-42c1-83f2-dfd8b62d2fe8
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 3dba393e-1ab7-4bbb-8ddc-7ec021063786
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 0d0d5330-553b-42bc-9a8e-abe0729969dc
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 3a7bfbf9-6dd5-4f1e-b6d3-2d8e98fd7dce
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: bf0afc40-4caa-4949-bb12-fa65a8b0bc4d
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 9abe0aaa-3ebb-4786-ada9-b9e23d7d9899
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 28c9fcdc-7847-4aa0-ace1-fda457c1de0e
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: a17ae693-d9ab-48a2-9e28-0aff2e7dc71b
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 261e0dd1-2a60-4633-8ff3-df303cd6bd9d
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 6cfcb686-af41-445a-9cbb-3ea13515e694
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 8e65a9ee-3149-4285-a135-c414f8e572f1
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: b1078756-70cd-486a-9b31-9b4b60e71526
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: c1538363-e3b3-4f99-b755-c6610304dadd
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: f81bb5ca-cf21-4144-9368-57879ba36a0b
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: f296440c-8ce2-41d6-8cfd-8dbf8bdd980a
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 64a8fcb0-4861-4ada-a0c1-3bc263ef4383
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 6f53242f-a464-4c7e-80db-028473419e91
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: abbaf27a-80ce-410c-a552-cb11895c256f
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: c3a09f50-2d2f-4610-8d0c-be8d8443381f
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 19fc17d2-4615-4dfe-a1c2-016fa42d2739
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: d6075286-4686-4960-8e47-218133a3a120
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 1c70a14b-da45-4f45-ac7e-25e2b9212955
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: e58a91b9-c3f1-4796-87d5-ffdd3bea9399
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 65e5b21f-9ea6-4ffc-89d5-948255cff066
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 088bfe85-70c1-449d-9995-86a3a761f18f
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 28b6912d-88fa-4da2-9944-a3b34edff8ae
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 99e1a08b-50b3-4750-8908-c239ab10ccb6
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 19741b55-1406-44c9-bfb5-48cff166734b
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: d50fd857-0b60-4ad7-8d15-bd965e5c1aab
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 5d3a9ab8-12e2-4135-8daa-64865ad8b274
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: f7627fdc-d113-4573-8533-c3073ab4d9e0
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: c99730ba-fc17-4f94-bccf-1b337846626f
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: ff1ec7ed-bbe6-4fde-93ce-d83fc2e37100
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: c5413fc3-370d-45ea-ace9-0592f1326a8b
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: e33004d5-ad7e-434f-93e1-f45f6b8c7cc5
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 353632f4-aa5b-4a49-8ba8-68ed51c66aea
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: d42aae32-eb79-478a-8e16-b71c82a2f6e8
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 6ac2a661-e8e3-400e-8805-dace7a2c072f
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 81e3f146-33cd-49c3-8f71-2fa9c03fae0d
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 3d10ce17-4d9f-4494-824d-ca6d4862a99c
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: b9c5fb83-43e6-4508-8058-e3d93bcdffdf
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 5f2843fb-0746-4765-90de-1e5ee21cc132
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 3782e779-27c6-49bc-93ba-95b88efd87f1
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: e307a154-7e8d-4a38-84b7-bc3cc7bd337b
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: d770335a-1bff-4542-b51d-d3496362104c
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 9f3e3909-be4c-415d-882e-94e2b856dd0d
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: ddd298aa-7057-4bcf-a1eb-4ef4a9a94126
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: c80a5798-13bd-4988-851e-fd6660c15dcb
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 40f572b0-6acb-4e83-822c-a08b35c2cabd
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 18d56a25-3b6e-4218-89f0-bcdf77fcdcd4
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 668bf0e4-bdd2-4aef-9868-c9a86535f1ff
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: c9119d28-821f-4611-9216-302c6a61de98
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 3b3669bd-dade-4b17-9b4f-7615ce6bc3dc
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 72a86b2d-321d-4c4d-adce-5244adfae651
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 5cd39789-7300-43ea-8321-88adf35db0b0
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: a62e2568-f069-467d-b858-416a531febc3
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 7b132c67-493d-4b3d-93ec-66df21206d73
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: d0d26178-82f4-4407-b76e-6e07c0d98590
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: a7a356cf-4926-4c47-81f9-db7aaf377199
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 07d2e821-1337-4eaf-be5e-bdce0315146b
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: e626a580-0e06-4ea5-8c63-bdb9998485c8
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 123cd587-ecf7-454b-9f59-332bbe765753
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: c0d53a9e-954b-4f7f-ad5f-6d7356c8a7ba
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 8fa9c470-ad40-4a92-a0d1-6a243cdad99c
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: f23851da-d573-4b2a-b918-798aa6d66501
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: b26cfa8f-45e9-4d0c-8135-bf69521b7eb4
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: b7991151-170f-42e1-b666-470fb7dc9f5d
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 04dc7c7c-8512-47bb-a9d8-5e0b7b539e31
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 26264a3a-582f-49ba-9603-ba8b1f4709e7
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 575e7658-f3ea-4bb7-bca6-1cfb80a29fd5
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: eb6e3830-4c88-448a-aa34-31f91b8e9f11
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 48281751-7b00-4e32-baa9-a6b7ce43021b
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 95f0ce44-8609-4595-b170-420a25be590a
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 69335d95-71c8-40e5-94e4-7f322f27bd35
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    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: 36db9693-d38a-43bc-b929-9ada3f9450bc
    creation_time: 2023-01-27T16:29:38Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.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_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound5.c
      input_file_hashes:
        ../plain/hard-ll_valuebound5.c: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound5.c
    file_hash: a93c350e5795e32421c3bef9d7525c3fd53f570f971d574def19132b3d6f08b8
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
