- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13253b0e-3159-4fdc-874a-0556b6775c56
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 5391437e-6128-425d-ae68-2375564fca44
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: f25889d2-9573-4ac8-9a26-3469dc583297
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 85f4ab51-f44a-42d4-b9eb-a36a2150d722
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 3344c977-8f30-47b1-be03-de8823d8e866
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 0e542df4-79be-45b3-b7f1-b012a2f1cfdf
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 07f29981-705d-4158-a146-bf54c3a9486b
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 14049ce5-5f73-480a-afac-4e1f1a0ce8a2
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 42971af8-da15-4b4f-b4bb-4fa2e6efa06a
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 1ca76d1c-0fcb-43dc-bd97-4a1f920f0ddf
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: a12b1b0d-9760-4dc3-8db3-fd7dc708bcec
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: f48b3d27-8586-40d3-9cc4-c3f5a7285ff8
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 1d710d86-53c2-43cb-bfd8-80c49c0e3308
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 32c4a3e3-990f-41aa-8286-a77088a744b1
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 8697b28a-8b65-47c0-b4c6-b9c4dc9f6a09
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: c3aec490-369e-40ca-9212-a960bb2203f9
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 2b332f9f-a5d9-4bb5-a588-11cb55ef57a7
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: cbde187d-fc9a-486f-b2cb-4513886d4513
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 7efce20e-d180-4da3-83ff-10cdf28ca93f
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 839ff417-9fb9-4c38-8555-5f696d972af3
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 5c58d69b-a67d-454c-9423-b0c758c9cbbb
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 1c3595de-4525-4555-9eea-9b2fdab111a8
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 02854f5a-b8b5-467c-986a-9d9a303a1e4e
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 6618e05a-32db-4051-a8d5-1b3d68544c90
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 67d7e669-96f2-4fb9-9057-281988b81da4
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 37d7c704-2b5a-41f1-9165-731532ffe076
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: f2a167f4-8e74-425e-b8b9-26b7ded2cd51
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: fbeed09e-da6e-4d85-aace-361f408b8981
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: ee86ba6b-81ea-49d0-b883-fb8cf20ae743
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 874a196e-e960-4efc-8331-ec22c8a8eea7
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: eb2f3c80-76a0-4fa3-85eb-512fc5bf447b
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 61fccbc0-7d45-474a-a64e-0ac6be3ce4ed
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: ecaba6ce-e78c-404e-a179-108c93d8c086
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: dfd62a54-a786-450e-b645-0c1dff702f8e
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: ef996448-b995-4fb0-b256-060eec4fcd82
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 651b64fd-e00b-4b1f-9e41-890dbaa42f6c
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 257f31f7-5a96-4679-a1dc-13ac1d512c3c
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 431dc356-8b40-4602-9f37-6cec2cdda010
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: c8dc717c-8615-495e-8ab6-c35cb99b1215
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: a10d2f4e-5815-4b20-be2b-829137170943
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: b1d8da58-83c5-4e45-a3eb-81e21eaf0394
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: aeb28eec-9104-499e-90cc-5d4706495b35
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 97686af8-fc76-4050-8ca9-a0569b50900b
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 0de87721-0550-40b4-b704-5193ca44bab3
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 77e7421e-84f8-4591-afcb-2168b5348c47
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 11afc1e8-c6c4-4af7-8dae-1b2e17d261ba
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 6a5e52a9-b9e6-4468-8dc4-4e4ca526108b
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 3c13eb92-0d25-4655-ba6e-1851eaae6f42
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: af52c3f4-f3aa-4d05-bf34-e334d67d09ac
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 58e8636d-6e8d-4d7c-9bbb-1311beecb2df
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 76c180ba-3f58-435d-84af-7a2c033973f8
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 41203860-3287-4a3c-beb2-46e2cdca46ab
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    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: 0a6df84a-f056-483f-a586-44b9ca979bda
    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/hard2_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound20.c
      input_file_hashes:
        ../plain/hard2_valuebound20.c: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound20.c
    file_hash: 1619c1c02ba7c9b660af32e6427e3b3d5cd6ca3ff286b9db386918ae0c8b508c
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 1 <= p
    type: assertion
    format: C
