- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0be484b-69af-478d-88b1-e09c196ff882
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 35
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7aa325a-eb17-4eed-a458-e3197eecbb0b
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 36
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a013091-9062-485f-9554-dcb69efed2aa
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 37
    column: 8
    function: main
  location_invariant:
    string: 1 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6233359-be65-4cbe-84cc-b982bee97634
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 37
    column: 8
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c68d4282-3921-4c1b-8361-81b8d70458b8
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 37
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06104c87-22cb-48f2-93b1-b66baf5864f4
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 1 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25433f07-1137-4fc3-8f70-8853b334aa4f
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 38
    column: 12
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18e6b394-63ea-4efd-b7b7-ea92e49a4bf6
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 38
    column: 12
    function: main
  location_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03180131-2f79-40cf-85b7-b34c04151d43
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 1 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14d2e745-2f5a-47a9-91f9-910db70576c4
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 40
    column: 8
    function: main
  location_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3337622-e551-47eb-a6a7-47fbe6700683
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 40
    column: 8
    function: main
  location_invariant:
    string: (long long )A - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43772f5e-79fb-4710-a1d4-ab72cb256532
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 40
    column: 8
    function: main
  location_invariant:
    string: d != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 339ffd6a-2e57-4f06-a46a-1ac3ee74f5be
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf50d3a5-7616-4de9-94b7-c6a356e96c8f
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 251ac862-d666-48ed-a5fb-3255769dc538
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 41
    column: 8
    function: main
  location_invariant:
    string: -2LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6d0a6a0-0b09-4e5f-ba90-db66d196636f
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL * (long long )A - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94d4b47e-5641-401d-8b97-085057a079db
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 45
    column: 8
    function: main
  location_invariant:
    string: 0 <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33c64c5b-8866-4222-a7ea-835a87e02f1b
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 46
    column: 8
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 771815be-02e8-4450-87e6-41954eb51de5
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 46
    column: 8
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ad7f3f0-7f4c-4e72-922e-ca42bcdbb799
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 48
    column: 12
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7861e483-4922-4203-89d0-f8fbb238b93a
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 50
    column: 8
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b56c162f-b6f8-4898-b4b3-5055774c8354
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 51
    column: 8
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bde61be9-4db0-4d7e-812a-ed91622ec589
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 51
    column: 8
    function: main
  location_invariant:
    string: 2 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a7a39a0-f4a3-476f-96f2-80e4d8f84046
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 51
    column: 8
    function: main
  location_invariant:
    string: d <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 086c9c1a-8f2b-43a1-b9ba-aeff3c2bfedd
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 51
    column: 8
    function: main
  location_invariant:
    string: p != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 45ffd188-ad5a-4bef-b37b-7fc4a46703f5
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 51
    column: 8
    function: main
  location_invariant:
    string: p != 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b56af41f-6ded-4ac5-8cd9-fd6ba18f6d22
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 570fbb23-c357-4147-944d-01e90af1d352
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 0 <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba1af1ff-6e82-481a-9538-34ceb1cdc37d
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 52
    column: 12
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 31a21646-7d21-4af3-9eda-e5094136f2bd
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 52
    column: 12
    function: main
  location_invariant:
    string: d <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 431dc7ff-ebe8-4795-95bd-f5fe768aa1d6
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 52
    column: 12
    function: main
  location_invariant:
    string: p <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 643f96cf-48f4-428f-957d-53dd2eb867df
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 0 <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c06192e0-20ed-45a1-bf20-3e24514af5f5
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23094156-5d6b-48a1-b3ed-44e4af2fc094
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 53
    column: 12
    function: main
  location_invariant:
    string: d <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53cdc165-0f95-4363-9f61-030b112d2bf8
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 53
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )d) + (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dfe9934c-3142-4d03-9338-d0e21711f31e
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 54
    column: 12
    function: main
  location_invariant:
    string: -1073741823 <= r
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37bdd4d0-ca21-4af5-ab67-686a625d056c
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c416d7e-ac83-4192-9f22-f2071fe34751
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 0 <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9ee28fb-24ea-4a2d-996e-ee932b2fe5a3
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 54
    column: 12
    function: main
  location_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac10251e-78c3-4c66-8d95-9f669f12ae2d
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 54
    column: 12
    function: main
  location_invariant:
    string: d <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc36099e-4ae3-4361-92ea-7a76a23905cf
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 54
    column: 12
    function: main
  location_invariant:
    string: p <= 1073741823
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f1568c3-d57c-45eb-b3ee-37e5ae5a86ee
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 54
    column: 12
    function: main
  location_invariant:
    string: (long long )r >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a5e7efd-05c9-4455-af48-75c79620d641
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 58
    column: 4
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1cd982e-625a-4e3c-b0cd-c1c7733cef14
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 58
    column: 4
    function: main
  location_invariant:
    string: 0 <= q
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 785a1e03-4c94-4ab3-be12-2f1f1e1e60c0
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 59
    column: 4
    function: main
  location_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44719428-20ba-498a-8bd9-c671a6cc8897
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 0 <= A
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f17bb3e-684b-42a8-8782-b35e028c72c1
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )A >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 448c044c-e089-4ba3-a03d-e5615195ea1a
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ce2ff7d0-0a02-479a-8428-bb6f675818e8
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1 <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e30f4cf-f282-454f-a8d0-48c4f8f0ad17
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 96253c80-d2e1-4d63-a8e1-3316b241cd4b
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 46f72acb-bb77-4490-9c0a-35067c007e75
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 0 <= q
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 07ad1b48-ed37-4330-8557-838b310ee1f0
    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/hard2_valuebound5.c'''
    task:
      input_files:
      - ../plain/hard2_valuebound5.c
      input_file_hashes:
        ../plain/hard2_valuebound5.c: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hard2_valuebound5.c
    file_hash: a077c1334c11d8329da2d0c58ca917b2036581fa7e949d1d304e3346ec54a811
    line: 44
    column: 11
    function: main
  loop_invariant:
    string: 1 <= p
    type: assertion
    format: C
