- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3a6ce10-5fd9-4466-a855-2f2e8e33ef49
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 21334e56-3182-430f-873c-4785b29485c0
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: df202a55-9ea0-424b-9cc1-9c670d5d8832
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 74cd1115-f34d-4c34-b418-887dcc0df0bf
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: dfc5b6b7-2a72-4563-881b-6c2445b6ccf2
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 3490bab8-fc95-4f77-9cf7-67f3093593f8
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: d33b62ed-a154-420f-9242-5fca50e6ddbd
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 197e87f2-81b4-4fb7-9ce2-be25d0753e81
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 53ff0508-09b4-4f72-92d0-be5fc3434c69
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: ec8d777c-f91c-4433-8f9a-513911ba1d03
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: fff2d84f-5f2c-4539-9194-aaa004b59ab9
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: b999383e-ef93-4b2a-a752-c5a9859bdd53
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: c22b101a-6de4-41f9-89dd-9b94f4f34c11
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: a7de7d65-1c28-4337-ac43-5123f01baa02
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: ae4efb56-f253-4236-9421-3cea9ccc5d83
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 122fb1a1-b8e9-4ae3-ac14-8958df071004
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 4c939ea6-ef6e-40c8-b156-94239edf27fd
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 5ef5eea5-3b8d-4644-bd31-f300a3ab7e43
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: ded191b7-adc4-45d3-ae4f-a319ae11bf75
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 9c1090ae-e731-4be0-b5ec-e69606956759
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 9890d91c-4818-488a-818c-a56032f6f59f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 4476b057-8edd-4ad2-9c4c-9483193edc98
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: c39d5c77-8232-4fdf-9841-346bdc2fe5f1
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: e8288770-62d3-4da2-a019-29e125e748b4
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 38226d52-eeb9-42d8-82f0-150d40bfd2b0
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 76c4d8eb-02e4-40ea-af08-6ec489b3e989
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 7788c73c-49c3-4711-845d-a1db6bad7f36
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 52334f02-661f-4f27-8ce5-71f3ea73b516
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 278e8371-d9e9-48d1-8db3-25efe4dfd71f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: aec37ba5-d64b-4634-acb2-76b5c73a829b
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: e3c4c5db-099f-4c4c-88db-a058f7aa7299
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 60414d86-0cf1-4975-828f-89673b64b529
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 2c001dd1-16a5-4518-9496-57a676dfaf04
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 59d476c2-b581-4cd5-97a7-538fc1a1d7dc
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: a53f3c95-f056-4a23-a9f3-12bad90c4b99
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: ff418c09-b235-467e-88c7-6151f2358178
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: f05f9dce-c7a9-48d8-ac12-0d1965544481
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: e4219d87-8a10-4199-8e69-9246fb36d971
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: f95cb349-663c-49f2-b2fb-16fb80cb648d
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: e892c5ce-ad60-4599-8969-a7c88c3350e1
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 8ea0d94b-1688-4eb7-a6a2-cdd2ba4d3f75
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 435edbc4-4b2b-4a51-8e8d-d6cdbe0cb28b
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: f5b9fb72-6c8e-4a42-bb57-334a4e71d48e
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 658134a7-3842-4799-b520-6857e0710300
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 3846f5d5-1235-4627-b00e-9078bdb8c05d
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 05cdd070-831c-4c05-bea1-734e43b42226
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 49234d98-520f-4fc5-96dd-e90d95036b33
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 2fd56e15-2685-4292-b65e-3865f22a2640
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: aeada88c-440c-4c10-99d6-208f526a25c0
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: d1eb6baa-e770-4e92-8934-597aa133b76d
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: fb923efc-f355-4772-8f7c-dce79ac3c79e
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 42fe0251-e358-4014-8226-eae25bc177b8
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    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: 7184240a-6f78-46ee-addf-e5969cf6b520
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound2.c
      input_file_hashes:
        ../plain/hard2_valuebound2.c: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound2.c
    file_hash: 39b9505d3a064a677b57bccb6de3a4c04e873275d34ee3c16e80371638b07149
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 1 <= p
    type: assertion
    format: C
