- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 722b822a-50e4-46db-a320-af0c30fe76bd
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 12087d53-9eaa-456b-8343-a9fa9c6a4cc0
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: b6cc3518-e6ce-4d41-bb82-1b255dfcde6e
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 31
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b84185b1-8f3d-4b23-b7c3-bcc6772e7aef
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: e18acdfa-9672-4b14-884b-04a9f3912968
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: d48b38c4-f660-46c2-b517-536eee48c442
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 32
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2454f207-2242-416b-b3b0-be02b68797c5
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 6b6e5aff-4327-4ce3-aeb4-61a5986e869b
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: b9bb3fa3-5064-43f4-bbd5-460bf51293a9
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 33
    column: 1
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 884ac301-69b6-4c1e-80ff-8cafcf2f6086
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 718b0594-fd77-433f-aa49-add8f0d6230a
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 36
    column: 12
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9393cf0d-dc1c-458e-aa17-10d44751e1ab
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: e24af465-f29c-4171-8465-eb594d295076
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48928771-5429-435b-87c6-4211125e7a07
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 41dd166d-4b7d-41db-8b13-21bc4d757de4
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 8734cc7f-e135-4e11-b4b4-bacff21ede37
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 2312a238-8266-4d6c-b815-cbaa37f6a633
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 445e529a-b511-4f7f-888c-db94cd97660d
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 421ac8db-8e1b-4959-9fa7-fe1dfe59ede8
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: f23177f2-e2eb-4b5a-8e2a-7069bb559cbb
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 03524458-46cd-488b-824a-0a8ae3502cd4
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: ef6fde1c-3244-4fa9-882a-e3d1a491fefc
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bcb4c2a-eebe-44d3-b799-76395d1c95e3
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 9a7e42c1-50ef-450d-831b-fdd6d904eb43
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: aa9f2aba-6ef1-4d33-8055-5e6bb95c8c05
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 44c6d15f-7df4-45d0-b7f6-0c0a78e5d99f
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 26f02873-337a-4b63-8dfa-87613d29621b
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 50e6802d-f244-4f8c-9847-0f5962d976d8
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: 545bd1f0-805e-4aa5-ad7a-9a60670eb16a
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 46
    column: 4
    function: main
  location_invariant:
    string: 1LL <= t
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ecfd2b61-0d5e-4c17-b5f8-ed1e1957c2c2
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: db754691-8216-4117-8c99-619410b4f274
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: a1571f98-0c9f-47e9-87c7-fe5fda5d3a4c
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    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: d80f0d39-226d-4220-945e-5d259f195c3a
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= t
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d0e61a88-d43f-4ef5-a68b-bbb8a42be945
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: counter <= 3
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f956221f-acc0-44fc-8e9b-5b6a549f4bab
    creation_time: 2023-01-27T16:31:04Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''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_unwindbound2.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound2.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound2.c: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound2.c
    file_hash: d6c389695f28ab23288d12eab23e55426fe9ec0f0b8fe9723cca18e00c3db8b7
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 2LL - (long long )counter >= 0LL
    type: assertion
    format: C
