- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b97f603e-a128-4fcc-9c0d-71674d9330ad
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 35
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fa6a19f-7490-4ce7-b6ee-7924ffe7b0d0
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 36
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 42676377-b135-48e7-b176-9654bc88dc1c
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 37
    column: 8
    function: main
  location_invariant:
    string: 1 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 999fa09d-5c69-4dbf-a58f-eaedc3b35721
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 37
    column: 8
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77837d0d-a261-4bfe-bc42-99b95f904f8f
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 37
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c48a4ba-3292-43a8-b26b-97bb12450936
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 1 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9c8c538-2860-47f7-85e7-0a74088298ae
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2c32098-e005-460b-b6ce-2fde2be52729
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 38
    column: 12
    function: main
  location_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f261d717-46b4-40ab-8118-b0ff036780ed
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 1 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b5055a2-3f9d-49b7-9392-bdd514b7e7ae
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 40
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df95e416-5b67-426d-8646-489d3ecd3fa7
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 40
    column: 8
    function: main
  location_invariant:
    string: (long long )A - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f90e6965-e9cc-417c-9040-0316b92adfbf
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 40
    column: 8
    function: main
  location_invariant:
    string: d != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6dce28a-3d56-4334-ad17-da19e7f21ad9
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8157d4d-7556-4097-8757-9c608ab8a248
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9c8bd85-be40-41c4-86d5-9e8edc634425
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 41
    column: 8
    function: main
  location_invariant:
    string: -2LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef7091a3-f2b6-4182-8682-3668f24d18a4
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL * (long long )A - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24f7ba82-c876-48c7-94c6-fe16598db674
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 45
    column: 8
    function: main
  location_invariant:
    string: 0 <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2170ed1c-37c9-465a-b6d1-d7eb48859967
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 46
    column: 8
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5831739-bde8-4a9a-890b-860243bf4710
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 46
    column: 8
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d3b97df-5b31-4bf8-a28d-06855b03e477
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 48
    column: 12
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a99b65f-085b-4343-b451-fe96ea557f8b
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 50
    column: 8
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21bbb6f6-cbf8-4b11-b739-ff19c1038899
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 51
    column: 8
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: feb228a1-e087-40f6-8808-7adc7f29ef18
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 51
    column: 8
    function: main
  location_invariant:
    string: 2 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a51f1a4-ad43-483e-a44e-a36ab8caf621
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 51
    column: 8
    function: main
  location_invariant:
    string: d <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e7dc112-f96d-45cd-8214-8516963ead8b
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 51
    column: 8
    function: main
  location_invariant:
    string: p != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4d8cda2-f9d7-48a6-a131-d0796a6acc80
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 51
    column: 8
    function: main
  location_invariant:
    string: p != 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7e85de5-8b6d-4ae0-b98a-91bd434ca28e
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a28235bf-832d-45c3-b092-f714928cc635
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 0 <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c3096305-eaf1-4ee2-b7b1-5fde51ff63e7
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae9c9b8e-0eda-4542-91b9-c9439162bec8
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 52
    column: 12
    function: main
  location_invariant:
    string: d <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 145ddc30-d9f2-41fb-9786-745d7088fa0d
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 52
    column: 12
    function: main
  location_invariant:
    string: p <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e324d73a-e128-43fb-bd4a-d6431c26f3f5
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 0 <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f33b8cd2-b456-46ef-a2c4-6cf74b9556dd
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c413e43-63bd-49b1-8d8c-a794122108ab
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 53
    column: 12
    function: main
  location_invariant:
    string: d <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d870363-b7a6-4031-8338-95506a2ac173
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 53
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )d) + (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8642fb6-9509-425a-9823-5f594f08001d
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: -1073741823 <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1a1a8ba-56b4-4ae6-b30a-c374f1de32f1
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4f668d3-b044-4436-bc6c-baab8e2200ab
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 0 <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1781ab0-bfb9-44ad-8747-4ef456f9c681
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25e72496-2b30-463c-9115-1d8adea6fcf9
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: d <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b047acb1-95dd-42ad-b270-708bc9f7f932
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: p <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ddd020e0-3d22-40a6-991c-7ea593e7545d
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 54
    column: 12
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef415aec-82d1-429f-98a1-8a4527e96ae7
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 58
    column: 4
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e2dea9d-abbf-43d1-a675-b133b84ff36b
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 58
    column: 4
    function: main
  location_invariant:
    string: 0 <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fec79f0-dbd7-4d67-924c-613f5a6ff901
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 59
    column: 4
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0109ab98-9ecb-46c6-8963-c58c7f476752
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 0 <= A
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab5ebe67-ddb5-4807-9bb9-3c00c07895e6
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a7d4ad94-27d5-45df-9348-e5250e5dc784
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e547cc0-f29e-4214-bfef-8b4630ad60d2
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d60ded0-eca3-444b-9bf3-0dc7ccaa083a
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 21530934-18aa-4424-8ef1-f4eb2a082c54
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c49b6b1-9e88-474c-a90f-3c562dbd6db2
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 0 <= q
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f230c9b-9ce0-4111-82fa-33ae4c245f1d
    creation_time: 2023-01-27T16:29:37Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard2_valuebound10.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound10.c
      input_file_hashes:
        ../plain/hard2_valuebound10.c: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound10.c
    file_hash: 174cfd8cb6426614b32355f584844d4fc6265ba8fd3c3cda6c788ade64de4fc0
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 1 <= p
    type: assertion
    format: C
