- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d892f07-b3bc-48dd-8d27-36722f4a6a2a
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 28
    column: 42
    function: main
  location_invariant:
    string: -1000001LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 816a4fa6-2f3f-425e-b668-1e26de16811a
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 28
    column: 42
    function: main
  location_invariant:
    string: -1000001LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8ca7a145-24fe-4a85-9d55-95b26e9b1ecc
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 30
    column: 5
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d83f7bf5-4f93-4dff-834f-ce030188de00
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 30
    column: 5
    function: main
  location_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9efdb3e-8929-4f3b-a2ef-3f56149586d6
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 30
    column: 5
    function: main
  location_invariant:
    string: i <= 1999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e43adc14-2c0c-4a35-a489-d1aed91a67c6
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 30
    column: 5
    function: main
  location_invariant:
    string: -1LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ba1571d-899b-4216-973e-b2ce580e86cf
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 30
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec2b92f2-5235-419a-84e8-5d29e2cce60f
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 30
    column: 5
    function: main
  location_invariant:
    string: 1000000LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db288560-f64f-4316-929c-e86828b47f0c
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 30
    column: 5
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1fdbd42-91ff-48fb-bd07-efc86417f187
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 30
    column: 5
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54a1b8e2-3a7c-4027-9bc1-7c73723c8f9f
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 31
    column: 5
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db5f9fef-ed98-4bef-9753-429fb81b2204
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 31
    column: 5
    function: main
  location_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8305fda-d096-4862-88f1-b9491cc95473
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 31
    column: 5
    function: main
  location_invariant:
    string: i <= 1999998
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12777534-5090-457d-9ea8-ca3e57f92aae
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 31
    column: 5
    function: main
  location_invariant:
    string: -1LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba4f59d6-7818-425e-9746-1e219d703629
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 31
    column: 5
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7afc6c0a-87e7-406c-8b80-3f3c1c84543b
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 31
    column: 5
    function: main
  location_invariant:
    string: 1000000LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eec28665-cdc4-4d09-b5c4-4ddc9a97ee38
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 31
    column: 5
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f4098ef-e83a-490c-a32c-4bb2ac502988
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 31
    column: 5
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03303cea-8394-4a72-8cb9-f48ad386342c
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 159c0e7b-6dc5-4c53-88ec-78fbd07ea063
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebab2110-e158-4cbb-9080-0734ab351825
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 34
    column: 4
    function: main
  location_invariant:
    string: k <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83cac764-37e9-4f34-8c48-64ddf27bc0bb
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c9b26d8-b01f-4b49-9521-079d7c69179f
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )i - 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e269ab7d-112f-4655-a1da-f4554814f21f
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47ff6431-80cc-425c-b92c-5f9810eeb481
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d77b00f4-1427-40d0-83b3-e38389e92cfa
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1560f7fd-3209-4479-a761-98e59c8b91e6
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 35
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09e8a1fe-978c-4f77-a5fb-3608e3fbce2b
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )i - 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49fc5c0f-8461-42f5-aedc-6af3cd57db04
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ccf7dc9-ed3f-42f1-83ca-23e4ad7b8f74
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0cbce8b4-6c2a-4588-8b6c-455afddd4d74
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 28
    column: 8
    function: main
  location_invariant:
    string: k <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae2d0cf5-5c59-4ca7-8095-2e0e5f1983ae
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 1000000LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: afc45588-97e0-4a2f-a07b-6d4e5414a758
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 29
    column: 7
    function: main
  loop_invariant:
    string: -1000000 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b181e3e6-98c1-4a41-94b9-930f78a01d82
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 29
    column: 7
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b79573af-0d8c-4854-945e-563c257ff2ed
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 29
    column: 7
    function: main
  loop_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e04be4c-4f4a-4409-ab1a-9f77db11962f
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 29
    column: 7
    function: main
  loop_invariant:
    string: i <= 2000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ef0bbf8-d00f-4985-b920-0e1ef62e7af7
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 29
    column: 7
    function: main
  loop_invariant:
    string: k <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5dd46fa5-6015-445f-93be-f1a232ba9045
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 29
    column: 7
    function: main
  loop_invariant:
    string: 1000000LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a196a690-5ce2-4aed-a092-17355e691780
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 29
    column: 7
    function: main
  loop_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f754adc7-0545-42c8-a975-2c3187ebd57c
    creation_time: 2023-01-27T16:29:33Z
    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/half.i'''
    task:
      input_files:
      - ../plain/half.i
      input_file_hashes:
        ../plain/half.i: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half.i
    file_hash: cd8ea842760c1d795b2a0ad721eea8bf94078967bffa91c75f5537bf4a53b968
    line: 29
    column: 7
    function: main
  loop_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
