- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56304f7e-a488-46d1-a7af-6732e46b4683
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 31
    column: 8
    function: main
  location_invariant:
    string: 0LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dbd5bb73-c252-40d9-9d35-4f7242332d5c
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 31
    column: 8
    function: main
  location_invariant:
    string: 1LL <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1d2c39d-7414-4910-8843-2c81737a8ec9
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 32
    column: 8
    function: main
  location_invariant:
    string: 0LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c47b4380-d139-49e2-8b58-9dcfdb215c74
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 32
    column: 8
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6ea9cd8-237d-4e05-aeac-f875ad898848
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 33
    column: 1
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba7d4a94-a550-4fe7-aefa-150a8568a00c
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 33
    column: 1
    function: main
  location_invariant:
    string: 1LL <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6641532-8e7b-42d2-a68f-b260e5a029ed
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 36
    column: 12
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8af22229-6aae-4f07-9d95-5f2988821e81
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 0LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7039c641-ab09-40a3-b083-7a57ba070d7b
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 39
    column: 8
    function: main
  location_invariant:
    string: (long long )n - s >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e03d2ce-38f4-4b94-9c69-e74e3c2bb3cf
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 1LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13cd5d64-309b-4462-a5a4-dfe2cf7c53c2
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 1LL <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d378e537-22d3-4756-a655-b80edf815d08
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 40
    column: 8
    function: main
  location_invariant:
    string: (long long )n - s >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ee22949-2768-4309-bfc4-ca4bd2e58f41
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9bfad0b-6737-4f3d-87ad-da9208dab351
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 3LL <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: defcf5fc-0a00-4528-ab04-a77b5f9cae2e
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 41
    column: 8
    function: main
  location_invariant:
    string: s <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca65f955-274f-41e0-aae4-ecf61671e084
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 41
    column: 8
    function: main
  location_invariant:
    string: (long long )n - s >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 554d169e-72ae-4a54-b22b-b16a294890dc
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 44
    column: 4
    function: main
  location_invariant:
    string: 0LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a273df6-0661-42f8-9eb1-85b73a5932cc
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 44
    column: 4
    function: main
  location_invariant:
    string: 1LL <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: defa19a4-4cd8-4852-a0bc-c7344c4d6653
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 44
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )n) + s >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc7a052a-6bb7-4fc6-bfea-b19367e29883
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 45
    column: 4
    function: main
  location_invariant:
    string: 0LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a554cb1-35ea-4f96-b174-e76a40d2302f
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 45
    column: 4
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bcfbc530-9694-43c5-97cb-2ec9b4693bd9
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 45
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )n) + s >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4fda681-6fe9-46e3-a1c7-66560a33b431
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 46
    column: 4
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fabe1472-4ea5-430c-92cb-2b4d846b437c
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 46
    column: 4
    function: main
  location_invariant:
    string: 1LL <= t
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 088c19ea-6151-44e2-90f9-b2dcc4a1e99d
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 46
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )n) + s >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d508ef2-8505-4867-ab6f-5e3a4a4e3596
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 48
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )n) + s >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65e92f97-7c9b-41a6-ba1a-d7898b5850c5
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a7c7e3f-6e74-4f7d-86c1-4544f5765291
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d00d6a3-0408-4078-9521-6f8602c07ed6
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 902c599a-0bed-45b4-940a-6d421779afd7
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 40f79d3d-f7d0-43c3-944c-037861957848
    creation_time: 2023-01-27T16:31:05Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/sqrt1-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound1.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound1.c: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound1.c
    file_hash: 0a70f1205afb9cca148fa8c17f899d7361834a55786fb03fe89056a7c6fb47c5
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= t
    type: assertion
    format: C
