- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fbf5a8bf-eb24-440d-b11f-9aedd7ceb974
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 966b906f-812a-4b48-a362-e071afe1ef2d
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: e2669c6a-85a4-414a-a803-1828afe780d9
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: da1953b2-3d37-488c-bb69-2c90108db7f9
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 5ada92b8-07cd-4fff-bd40-0198451787f7
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 77136528-2863-4e91-859f-690b03ab290a
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 30a92966-02c0-4d90-9abe-e2e3ebc66274
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 69302774-8b47-4e85-9da7-4a6e6933612e
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 9c19b202-7f1d-4708-9a02-b1b6001e9091
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 9921a347-1d2f-43ed-bd2c-4d9672494888
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 95dac2da-1dda-4c53-ad07-2f2d8dc59ec1
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 69ed8a1c-ff89-493d-af47-fd757738c877
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: b275adaa-2a54-41bf-b164-a0f56dc4d019
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 5bdbf5cb-b5cb-43d2-b68e-5fae5632f242
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 2248eb5a-57e9-4793-82e8-499b123e75fa
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: d66b7f48-2970-4728-805e-308072642f6a
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: c59b64cc-0226-496d-82bd-435e0ada5397
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: c96ab2c9-ef4a-4db9-a4bd-6c2933c4eaeb
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 38a83525-01f5-4b35-bed2-9e3dced3619c
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 63336c5c-5a13-4dd0-9eb7-7c728f7d3ce8
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 8c648a68-651a-464d-b584-36235b93dd9a
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 05d54f9a-8959-428d-a430-9f65ebf50f34
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: ad57b6dd-9aee-43f6-b949-23e6347c2b82
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 0f0d9083-9506-4a70-ae54-ebb02b31eb4c
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 33c78702-5e01-40ee-a28f-54f328d12311
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 8ce447a4-8a55-4dee-af42-5d5acabadd89
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 08549edf-8dfa-4790-96c3-4ad6f69a4ec5
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: ad36a2cd-d775-4006-b447-9dd63a79b182
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: d49e9f84-4701-4688-9858-5b247de7cf20
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 512a1e3f-0e85-48ad-b867-a5a522bf21c8
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    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: 4c80ea7d-219b-4ae1-9e15-7e511fd22511
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_valuebound50.c
      input_file_hashes:
        ../plain/sqrt1-ll_valuebound50.c: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_valuebound50.c
    file_hash: 5cb4924cbdb465eb5009b33592f9047ad895ad10dbe627600c12529f62c9845d
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= t
    type: assertion
    format: C
