- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36496f36-900c-4cd6-99b4-a31d77bf9492
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 4bbbc9ba-8b56-484c-ba46-665977c9b815
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: a8e1c012-a3b3-4eb1-8819-db1aae840930
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    line: 31
    column: 8
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d38c837-f53d-4b9f-8e66-f94ec8f84767
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 15974bd2-5e46-4e65-8930-e80e209421bc
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 60aff5d8-a1b2-4b41-90e8-4d23eb0e4b38
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    line: 32
    column: 8
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 403ce670-651d-4512-9bf0-0b9a0a79f9b7
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 4d570c69-afa7-41b3-bead-b1e5e68c0e60
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 6c3348db-aee1-4d98-8b5f-8b16ae91f5d0
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    line: 33
    column: 1
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb77938f-d527-460b-aa11-07db8a07018a
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: a20d93bc-270c-43b8-bb1e-d0ec86dd5052
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    line: 36
    column: 12
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c050490-3f02-4eb2-b556-565f5f0da97d
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 8bf36cee-c73c-49c1-afab-836c67d55620
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a399ff52-fabf-4a1e-bac9-82d05b360217
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 9f986ca6-2886-4f73-bc15-dbd927845b15
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 03689d88-d6d9-47f0-9005-1010319b0647
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 6139d177-af45-4705-9310-5aee09df4abf
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 988ed3c6-6a21-44af-a92f-0e3961cf5217
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: f4d468fc-a214-449a-b775-eeb7921072c7
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: d4535f70-48e1-46ef-8659-4b227714b42c
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: b98e9f2b-6e94-4fc4-a939-8d4ea0e2e1b1
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 0a233dc0-8fa9-4c2d-93f5-a9d48ced6083
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 514ca0f8-78d3-431f-ac06-9c596f679c87
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: d4b2ed8a-5610-4c9c-9316-a52b97e38d81
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 01b14b43-cf28-45ff-ae6b-9771d124c1a9
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: fd5fe68d-7ce5-48dd-835d-bcbb81cf708c
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: c394253c-6579-4123-bf74-a4d46a285ae7
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 4ceb3076-d282-4dcc-b09f-0329ff88284c
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: f1115c25-b7c1-48b3-8ca8-e140676ba086
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 955ca4ba-5502-430b-83cc-fe58a9b5965e
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 4dd54574-f92c-4b2f-9b29-7431e3ab1dfe
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 6e38bc39-ce7a-4b5d-92b6-722dfe9eb933
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: 79affb91-24cf-4760-955a-23e7009235ee
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    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: ad331f35-6404-497f-aad8-1e180f6baf86
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: counter <= 11
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f3fe5b7d-686c-42ba-bccd-66e13fc5d7e8
    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_unwindbound10.c'''
    task:
      input_files:
      - ../plain/sqrt1-ll_unwindbound10.c
      input_file_hashes:
        ../plain/sqrt1-ll_unwindbound10.c: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/sqrt1-ll_unwindbound10.c
    file_hash: 4615816b63186e8ef25ffa56a09fb574b90534edb7a787dbb36e36eb2c34dee2
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 10LL - (long long )counter >= 0LL
    type: assertion
    format: C
