- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d295774-5c98-409a-89b8-8efc86497913
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 41d1e0c3-fc4c-48bb-9de2-0b3159bccedd
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 752dce19-8dc3-4a70-9c54-86d360a8112a
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 0de16db9-b5f6-4db5-a832-0b3d9caca1d6
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: e0d10b3a-74ac-4c73-addd-202a2ebf8517
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 069edad4-8856-4133-a522-5272d295cef1
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: b19b7c37-5a0f-4d41-8806-2942775f6415
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: b408a547-1af7-4e82-a8cd-f49ef63b94de
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: fd68d6c8-10fa-443e-9281-33a1fcc484e6
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 0a720f40-68e7-4704-a365-70ad149165a4
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: dd1c402b-0b07-4a9b-b065-7f81b62dae3f
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: d240497a-fa72-4c72-8a41-e520a99bd2e5
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 22c38e90-98c9-4fec-aa3c-1b7d5fe51d55
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: d94221c0-9568-45c5-ab6e-7d4d2e9daf20
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: a9bfcca4-1ecd-4469-8d43-05711de048d3
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 7fb81a2e-e6bb-4da5-b545-0831932f382c
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 8042ffb1-a596-4e4c-9f2d-590238155da8
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 68dbb103-9b58-4abf-8400-9ccbb84496be
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 83ee8762-dd85-4f26-b866-be823357123e
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 03be78b3-531b-4bf7-8716-9c706b42eb14
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: c99255ec-27b4-4bb9-9883-3d255896e3c1
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 13f050b5-c321-44b1-8e4b-3b3ffc35dfd2
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 046dcce4-3c72-4628-b9e7-7b6fd6f4de1d
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 876b6aff-737b-48fc-b4d7-732b6081d80d
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 6001105d-84f0-4c32-8b4c-0367945b2954
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: c2fd10c1-dc45-4d22-9897-205d347cc93e
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 55cdc6e9-7811-40ab-b06d-bce1166d4c84
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 770404b9-95e7-4ef8-83f0-7ac0835092a4
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 43ae160a-0825-47a1-ab3d-0ef39fc0ef94
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: 6e0c80f4-48f0-4c39-a1da-399b0bcb2c9e
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    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: e7cb5f16-552b-4e51-a49b-8ca2b74554a9
    creation_time: 2023-01-27T16:31:06Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_valuebound20.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound20.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound20.c: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound20.c
    file_hash: 070b005151a155625f2a1d89ebf21c03a6d381af2d7b663a2fe06061e79da5f4
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= t
    type: assertion
    format: C
