- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 433db90d-eb94-43df-828a-9d316c932db4
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 40285faa-aa08-49df-9ee9-a6a72f58cb6c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 734443e0-7f18-4010-9ac3-9009431db073
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ca216cf-9430-4132-8b96-c9cbeb4e9b69
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: daea226e-309a-4f1b-aa3e-c4834c029594
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 112b1890-06b7-4072-a6c4-ce46399789f6
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 32
    column: 4
    function: main
  location_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53f3828b-e12c-4814-ab79-3fdfd943b74a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d974395-909d-48c0-b94c-9b87f57e8fe6
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 33
    column: 4
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1d9ca10-0e2d-4a1e-bbd9-1c58c0a7e72f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 37
    column: 8
    function: main
  location_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5bea6f7-8ab4-4d4f-954d-63e4242aa46f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 37
    column: 8
    function: main
  location_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a30e4ac-8fb1-4451-a0d5-d9d89d9c665d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 37
    column: 8
    function: main
  location_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5d16415-16ad-416e-a391-549230626ded
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 37
    column: 8
    function: main
  location_invariant:
    string: (2LL * (long long )A + (long long )B) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e81ea811-9e8b-465b-86cb-d3d2a897a246
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 38
    column: 8
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e8fd17d-175c-47b2-9353-2ed28fb82b69
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 38
    column: 8
    function: main
  location_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c688ae88-6efb-4847-95a4-f6fbc46bf429
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 38
    column: 8
    function: main
  location_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af1ac60e-ef40-4805-b8c9-78d299656cb9
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 38
    column: 8
    function: main
  location_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa9ac00a-379b-4a0d-8b54-80a70e715994
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 38
    column: 8
    function: main
  location_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b350db74-b391-4a16-ac8f-ec2e6b98397b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 38
    column: 8
    function: main
  location_invariant:
    string: (2LL * (long long )A + (long long )B) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b85c771-af45-47ed-a0ea-26f9c0526b8f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44206843-9dfe-4380-82f0-780a14d6cbbf
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc273bb7-1363-40cd-aebb-5e2ac920a034
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 39
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 825ac16d-aa77-454f-b9c4-1ad7661540f7
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 39
    column: 8
    function: main
  location_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 408b3abf-b06d-4389-8dc8-efa384e21dfc
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 39
    column: 8
    function: main
  location_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48b38db5-ee66-44cc-b17e-65f23784d3b1
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 39
    column: 8
    function: main
  location_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 730ac289-9c23-462c-9a03-74b27adf1f2a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 39
    column: 8
    function: main
  location_invariant:
    string: (2LL * (long long )A + (long long )B) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4218dec8-8e63-4090-8941-f568b5e4fd3d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ada21ce-167c-4cd0-a8dc-dba655c49282
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 52cfd4a1-915c-4475-90fe-f7f5d28b22fb
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f54799a1-3ecc-46bf-a03f-5ac73388d0ff
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 40
    column: 12
    function: main
  location_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3181bcba-62d3-4ab2-94d9-8db03fb860c7
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 40
    column: 12
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32d29dcd-a7c0-470a-888d-9c2f174a8f3a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 40
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd5122f1-2b41-4da2-be4a-c2c80a161dea
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 40
    column: 12
    function: main
  location_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b9874f9-8499-4221-b5db-96a143f1f94c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 40
    column: 12
    function: main
  location_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d80d31f8-7f42-4030-925a-4c1e83daf6ce
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 40
    column: 12
    function: main
  location_invariant:
    string: (2LL * (long long )A + (long long )B) - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73ae88a4-3600-4975-a8bd-31b677de92e5
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a0a95bb-1de0-4edb-9565-4767546dc569
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 42
    column: 8
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4df91f2-6001-4961-91e9-b58642811b55
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 42
    column: 8
    function: main
  location_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b155dcd-689e-46b5-8608-1d46a0864c8d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 42
    column: 8
    function: main
  location_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79b9cd2e-2ad1-4176-a383-9109ae22db3e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 42
    column: 8
    function: main
  location_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8941b92-4cfd-40a7-b0bf-9c008ed4ed82
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 42
    column: 8
    function: main
  location_invariant:
    string: (long long )A - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23503d1a-115c-405c-bd10-8e1afde9203f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8b75b18-b255-4ac9-87aa-7c137d91f88e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5bbc1b3-0bd3-4eaf-b7ab-c340f4cb9d2c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 43
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0ed710b-9af6-4b08-ac44-35704c0e32ed
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 43
    column: 8
    function: main
  location_invariant:
    string: (0LL - 2LL * (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 119b3d69-3910-4267-9484-1d82066cf57c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 43
    column: 8
    function: main
  location_invariant:
    string: ((-17179869180LL + 8LL * (long long )B) - 3LL * d) + 17179869180LL * p
      >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ced7498-cb1b-49f3-9909-2f4a377b8273
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 43
    column: 8
    function: main
  location_invariant:
    string: ((-8589934590LL + 2LL * (long long )B) - d) + 8589934590LL * p >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 308d42c7-6d1d-4deb-b576-a3d164fbdf66
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 2LL * (long long )A - d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d41e24a6-185d-4281-ac9b-0b68edfd26d2
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 47
    column: 8
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17a4057b-2460-4269-a414-f0f64b4a8281
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 48
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fee547de-1743-4172-bf1d-8819f257388b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 48
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a82249b-e73a-4728-b2f9-ac6712f28189
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 48
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29cde046-fed0-4dda-86db-a90607198976
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 50
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e2bee45-3f98-4191-b418-9afdf334b9f3
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 52
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97224b90-2af7-4f5a-bac4-20e08fd7061a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 52
    column: 8
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ddbf001d-3efc-4599-9e68-95d760fe1b39
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 53
    column: 8
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c1c1666-1f58-4b4b-a59c-60f823f4ff6e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 53
    column: 8
    function: main
  location_invariant:
    string: 2LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72786fc6-4d40-489a-a0f1-696f3028fa85
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 53
    column: 8
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac165cfa-3afe-4137-a375-749b40a5db6d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 53
    column: 8
    function: main
  location_invariant:
    string: p != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d9531e5-434b-4edc-bdda-a305069829c6
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 53
    column: 8
    function: main
  location_invariant:
    string: p != 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb97a9f9-46ab-430b-843f-e745106b6f11
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8ffbfb3-d743-468a-855b-84b05aed00ec
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48bb7734-0451-4997-ae18-05b8ae528ead
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 223cdcc2-7640-4f9f-9e29-eaaaf882f3a6
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 54
    column: 12
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25b172f9-55f4-4685-b653-981869a95334
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 54
    column: 12
    function: main
  location_invariant:
    string: p <= 4611686018427387903LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a90edfc-bf28-4c2c-a808-6cd16a7b0b20
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 55
    column: 12
    function: main
  location_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f885c4da-d5a5-428f-a2af-40d29fe55349
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 55
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f42dc663-1f18-460c-9b74-a4867f78aec9
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 55
    column: 12
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a646812-09b8-41be-99f5-baff482d9e34
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 55
    column: 12
    function: main
  location_invariant:
    string: (0LL - d) + r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4cc4691c-77da-4ae8-82eb-b42e6a8f8466
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 56
    column: 12
    function: main
  location_invariant:
    string: -4294967295LL <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 463c6717-f5bd-42bb-b430-98975930462f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 56
    column: 12
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 00ccf272-d798-4705-81ff-0f8b18d73d7c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 56
    column: 12
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0020d0a0-5d08-4a62-b831-2a3c0a2ed48b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 56
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a704361c-3217-43e3-a437-1db122f71b2d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 56
    column: 12
    function: main
  location_invariant:
    string: d <= 4294967295LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc05c537-dba8-45a2-b032-a26aee3de6ef
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 56
    column: 12
    function: main
  location_invariant:
    string: p <= 4611686018427387903LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5e5492e-1a5e-43ba-91ca-72fe545e749e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 56
    column: 12
    function: main
  location_invariant:
    string: r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7f61228-fc8f-414f-bbfd-29809b13aa79
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 60
    column: 4
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27b531c3-a198-4a10-b987-d9c59ef5e761
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 60
    column: 4
    function: main
  location_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25aaf178-3fe8-40a1-85d1-ace3b0a2edd3
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 60
    column: 4
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45f046c1-0dee-4ace-8c27-d2c4804a3857
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 61
    column: 4
    function: main
  location_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5df1efed-7c9f-4320-98c7-5dcf9c31f654
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 61
    column: 4
    function: main
  location_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a2ccaf3-da07-4bcf-874a-f63f24a35184
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f6acb70-ceab-4b2d-82fb-9fd41501a517
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf9910dc-123a-4941-82d3-c2439107862a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9266cb2a-dc08-4e69-8577-055bf4a3fcdd
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bdd9db82-cbef-467b-9b40-90471610b870
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 113d1884-0b4e-459f-8547-12111cbc3c3b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db4b7652-285a-4c45-a6d8-315ee609df9d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7939fd45-0c64-457c-b555-85039a95cd77
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )B >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d5c13027-d9f8-407f-8ee4-e62184652565
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= r
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: db1a1b66-74b9-41f2-aa03-db3df84f984b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 49cf18b1-567b-4aae-8f92-4d4eddc1346b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f79c77f7-1720-4e50-bd56-44c36bb565a0
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: r <= 4294967295LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b6a5d548-1a22-477e-ae23-fa1dee3200fe
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e37f451-4c37-4385-98df-26cbe68c91c4
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: (0LL - (long long )B) + d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 66de61fa-9d39-4892-a550-fed4d88a1b62
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: ((-8589934590LL + 4LL * (long long )B) - 3LL * d) + 8589934590LL * p >=
      0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cb3efa74-e60a-4adc-9db4-494f1aebf768
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: ((-4294967295LL + (long long )B) - d) + 4294967295LL * p >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 98888ae7-da66-434e-af9e-8db8ae097718
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: (2LL * (long long )A + (long long )B) - d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ab7e93b-c5d1-4c4d-b4f0-519d3c4e9d09
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d2d98405-b239-4bae-8c6f-a795bd8fe365
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= q
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c8bf79d5-10ed-4cc9-8230-1eaa638c094c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 53df84cc-521b-4fe1-83a1-14c1484e5f24
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/hard-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/hard-ll_valuebound20.c
      input_file_hashes:
        ../plain/hard-ll_valuebound20.c: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard-ll_valuebound20.c
    file_hash: 6977cec8a403ff3f16926270da45a38f7b1f51a39c72ba3797fb74b9637fd796
    line: 46
    column: 11
    function: main
  loop_invariant:
    string: d <= 8589934590LL
    type: assertion
    format: C
