- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 497d60a6-ae9c-471b-860f-c74a37f5f6ac
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: b7565eeb-7a1c-4692-88d0-232dbfe0138a
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 196e9abd-5ca0-49aa-92cd-3163752ececb
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 0dab89ef-7823-4cd0-a4cb-cc8663b6aab2
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 4f1e7d81-5b29-415f-84f8-fba02e2d0d68
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 8dda7bca-3618-44ca-b6b7-f72a0f42795c
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: ce2dc4d5-3389-47b9-a5e2-ba54f02b8e73
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 27d8942e-08b9-4186-9f40-ec418a477c12
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: f22c9273-f593-49c6-bf82-09cc8f19c084
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: c3eba369-136c-4596-8dc9-0a9ae06bfed5
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: a62aef57-3764-4334-a1d4-93271ce286be
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 66e5623a-8918-4be2-8a45-df21efec19bc
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 22b3afbe-a8e0-486b-8f04-adf3a19b597a
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 90e12ae0-3435-41d1-93d5-eaf8b51a1156
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 8cbd93eb-a5b5-4935-9ec1-6054e6bf6e42
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 13a34254-47cd-4ac6-8a0b-6852f837b348
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 9ab06f6e-6107-4f28-aaef-5b58e3d59778
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 55ecae3c-19ec-40e5-a06b-d332360ba762
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 55947650-bb68-4147-98e9-ccab8ef465b4
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 4da738ff-d6be-40b9-80b7-3e916504ca3a
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: f0412bf7-d0ff-4d7b-866f-c0d0a1cc3cbc
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 296d9861-daa6-4078-bc1b-6103284ad8b6
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 152ed1c1-3988-4c55-89a7-e661de48699f
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: bc2be3f7-948f-4da8-a01d-99de0d6f74b0
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 3a44a835-c9ab-4928-a591-53409fe7b9e4
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: e5713944-4dee-4d39-9f98-1f159efe0ba8
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: e7dd2249-89f8-43ba-a8dc-67cb67f875ea
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: ce6c239a-ce9f-439e-bbc9-02bffe3696a0
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 2fa3d149-47bd-46b6-ada5-5b8dddf10741
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: ba332e14-e74b-4942-967e-5c4bac8d5ac2
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: c357ea39-1b67-4aee-8980-eaaff65719da
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: a526a7de-4239-49bc-84bc-aef939ec385a
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 46154650-b8c9-45af-90a4-59d604b2a61e
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 84180c95-a6ab-4ceb-ad75-860da84b2d9e
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 4dcc6018-3861-4901-a765-567bb3cafe8d
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 45856eeb-fcd9-414e-8e78-9f8f1d44fc90
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 3a344e1d-a5d8-4c6f-a9b3-860b1fe9af9e
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: feb7eae5-af9f-4e8c-911f-a18a24a76b24
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: fec6d5d1-e3e5-4ed3-9081-cc51a3906ba5
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: d0c1ecce-5fc9-4a35-8a4c-076e537815e9
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: e3d11c4d-b3ac-4861-9fb6-bd5311e4c975
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: c2e58d81-a0d5-42d5-ab7d-c4f46ef7a7f7
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 9cb7b004-7787-4ddb-9161-8768ed724a79
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 0ab44b58-70b4-4e8c-ae54-f95124533943
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: f13c3399-6d81-4cce-8c59-6cd929187941
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: ad7190ec-f94d-48e0-b2c4-1f9fffd158e1
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 666e80de-cef6-4496-972b-4cf7d30151a2
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: e9a92ddd-8a66-44fc-9c53-5cdb9cadaf0d
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: a1aff686-6750-4d88-af96-285d862ed411
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 3b4071e8-9731-4333-aff2-80e0f789cdc9
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 1805afbc-9cfc-4dc9-86b9-8839ade4e712
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 6b139cf6-243d-475a-88b0-0b3fd6036e75
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    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: 31c7a9fe-0e56-419e-b04c-bb7a9a43b3cb
    creation_time: 2023-01-27T16:29:36Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound1.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound1.c
      input_file_hashes:
        ../plain/hard2_valuebound1.c: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound1.c
    file_hash: 45ff7b74faf4250f77b788e07275d725ea3dbcc73af0b2b0d64dcf5aa7f7b78a
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 1 <= p
    type: assertion
    format: C
