- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb271826-7755-48ed-90bc-2241a60dde5d
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 31
    column: 4
    function: main
  location_invariant:
    string: k <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4425587f-fe11-4fd9-909a-8b821c28edf1
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (-2LL - (long long )i) + 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b8ca077-5f61-48cf-9f04-85124486e1d3
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (2000000LL - (long long )i) - 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0e8ba1b-f176-4d5b-bcbb-c5f7105762dd
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0306914-132a-40e7-86cd-404480a4b8cb
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f31a0f7-3e30-4204-b0d5-cb79685e3388
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7105e0e-2cb9-4379-a035-96a7f9303255
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 32
    column: 4
    function: main
  location_invariant:
    string: i <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 603ccf04-d376-4f6f-9ed0-b541028c1d71
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 32
    column: 4
    function: main
  location_invariant:
    string: k <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ecf6bdf-1e66-400d-a2b3-9a57f154cf80
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (0LL - (long long )i) + 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d623b83f-b95b-42aa-947f-f0ed1b3cead6
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (1999998LL - (long long )i) - 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89034548-9bf1-4d77-a7e0-c1f07e2f10e3
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5f37f71-a8f5-42dc-82fb-524c7bd949c6
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 34
    column: 6
    function: main
  location_invariant:
    string: (2000000LL - (long long )i) - 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ead6c5f-0f70-46df-a4c6-44fa51be91eb
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 34
    column: 6
    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: 59e199db-9b30-41c4-8ed7-fb84143c31d6
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 34
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de59b383-c0e2-4a24-8dda-2b08c4f1d6ce
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 36
    column: 4
    function: main
  location_invariant:
    string: k <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96b17cea-36e2-4823-b887-9c09009593e7
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 36
    column: 4
    function: main
  location_invariant:
    string: ((2LL + (long long )i) - 2LL * (long long )j) + 2LL * (long long )k >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c08b477-4275-4a64-ae70-bdef48202807
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 500000LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0cf46ebc-1f39-4dda-83dd-8b8ff58384d0
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 36
    column: 4
    function: main
  location_invariant:
    string: ((2000000LL - (long long )i) - 2LL * (long long )j) - 2LL * (long long
      )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad02f691-80e3-44bf-a5df-252fc9d019c3
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 36
    column: 4
    function: main
  location_invariant:
    string: ((long long )i - 2LL * (long long )j) - 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01bba930-0000-40f7-834e-cb04c9505f95
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3f9cc04-130f-4b23-af40-d314f667f29a
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bd2f8ec-4c6e-454e-9017-a40c06cc18e3
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 37
    column: 4
    function: main
  location_invariant:
    string: k <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44db236c-b0a9-4e54-ac3e-c8b1eb96480f
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 37
    column: 4
    function: main
  location_invariant:
    string: ((2LL + (long long )i) - 2LL * (long long )j) + 2LL * (long long )k >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8cb4b068-03df-4b89-81e6-7dc32f4a1ce1
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 500000LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2b16c78-9e26-4a54-b358-df52f461619f
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 37
    column: 4
    function: main
  location_invariant:
    string: ((2000000LL - (long long )i) - 2LL * (long long )j) - 2LL * (long long
      )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f31c6a8f-7b8c-4052-adda-2b0c13bdc697
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 37
    column: 4
    function: main
  location_invariant:
    string: ((long long )i - 2LL * (long long )j) - 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc46ccf1-30af-4843-b39a-ab2f40689cdd
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 37
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03a3b9cd-146e-4c5f-84bd-2b4860c4380d
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 37
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ed714f6-fa5c-4e47-a28e-35ee334c39bc
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 38
    column: 4
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01123d0f-3594-4315-a1e3-04b5af4ed2f2
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 38
    column: 4
    function: main
  location_invariant:
    string: k <= 499999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 279c6b02-b26c-486e-8ded-f16f2130a689
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 38
    column: 4
    function: main
  location_invariant:
    string: j <= 499999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4599b20c-3079-40c3-a0bb-5f62d093f8ad
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 38
    column: 4
    function: main
  location_invariant:
    string: ((4LL + (long long )i) - 2LL * (long long )j) + 2LL * (long long )k >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 416afde2-933a-4437-a948-535ca0774b23
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 38
    column: 4
    function: main
  location_invariant:
    string: 500000LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0b82f66-5363-470f-b953-3608a9c2956f
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 38
    column: 4
    function: main
  location_invariant:
    string: ((-2LL + (long long )i) - 2LL * (long long )j) - 2LL * (long long )k >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cbc1c0a3-daf3-4a7f-9fe1-da1dbe7ffb14
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 38
    column: 4
    function: main
  location_invariant:
    string: ((1999998LL - (long long )i) - 2LL * (long long )j) - 2LL * (long long
      )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f6ed67e-b063-4d5c-978d-7370d7661b4f
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 38
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb0f6bbe-17f8-4946-b58c-988100af41b9
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 38
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 91d07d42-ca61-4766-a4ca-24f5fbc7fead
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 40
    column: 2
    function: main
  location_invariant:
    string: ((4LL - (long long )i) + 2LL * (long long )j) - 2LL * (long long )k >=
      0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17517c0c-7f6b-463f-8851-668ca8177ead
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 40
    column: 2
    function: main
  location_invariant:
    string: ((2000000LL - (long long )i) - 2LL * (long long )j) - 2LL * (long long
      )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cfa22d9-b38c-4fbc-b9e1-98f186824465
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 40
    column: 2
    function: main
  location_invariant:
    string: ((long long )i - 2LL * (long long )j) - 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad8148e9-f654-46a8-9bbd-f8309129f6b0
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 40
    column: 2
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36b17935-2043-4be6-8b9d-55d2aea32361
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 40
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75e8e6cf-3fe4-4c91-8ad3-57be5c2c67ae
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 27
    column: 23
    function: main
  location_invariant:
    string: -1000001LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86233271-64b8-4d65-8012-b5b96a9c3e1f
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 28
    column: 2
    function: main
  location_invariant:
    string: n <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de66cf84-a4df-4c1f-8fd2-a151fa282318
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 28
    column: 2
    function: main
  location_invariant:
    string: 1000000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 506f483a-d516-4f49-bf95-67d79f18d69b
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 29
    column: 2
    function: main
  location_invariant:
    string: k <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ad3020d-32ac-4540-ad84-c812955f47e0
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 29
    column: 2
    function: main
  location_invariant:
    string: 1000000LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b3c0ebe0-c871-4f91-b0ac-db6d9e041e68
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 30
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c03196be-b248-4e43-a10a-0989cf1fa20a
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 30
    column: 9
    function: main
  loop_invariant:
    string: n <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 74ffed8d-a29d-4aac-a6b5-1e03bbcc3018
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 30
    column: 9
    function: main
  loop_invariant:
    string: i <= 1000001
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bc19f9b4-1a5c-4624-8686-78185924955f
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 30
    column: 9
    function: main
  loop_invariant:
    string: k <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d4996b32-669d-4bdf-9b92-0f6d2691be50
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 30
    column: 9
    function: main
  loop_invariant:
    string: (2000000LL - (long long )i) - 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 024d0aa2-f345-4ef0-81cf-0116336c3ef6
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 30
    column: 9
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c5c84484-00d0-4c74-a99c-c93c0908cf4c
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 35
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b28b0a3f-964e-4623-aec5-fdfb74a5b7ee
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 35
    column: 9
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 67719bf6-a3cd-4ca5-8a74-3ffaaf473ad3
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 35
    column: 9
    function: main
  loop_invariant:
    string: n <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 82876ce1-ee0f-440a-95b0-c3f82591e8f4
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 35
    column: 9
    function: main
  loop_invariant:
    string: i <= 1000001
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f83258eb-cb17-4788-89ea-65f9276fb406
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 35
    column: 9
    function: main
  loop_invariant:
    string: k <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 621185f1-157c-422b-9fa0-21516e06259b
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 35
    column: 9
    function: main
  loop_invariant:
    string: j <= 500000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a280e6e-7b8d-46d7-8d0a-d90e6ce9ee13
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 35
    column: 9
    function: main
  loop_invariant:
    string: ((2000000LL - (long long )i) - 2LL * (long long )j) - 2LL * (long long
      )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a4c6442-2ea8-42fe-bc4b-6d3480ca358d
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 35
    column: 9
    function: main
  loop_invariant:
    string: ((long long )i - 2LL * (long long )j) - 2LL * (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6508ef26-8cf7-4d1d-932a-46adcd63840f
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 35
    column: 9
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fe6c5bc1-ed09-46b3-bf81-1f83d654a276
    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_2.i'''
    task:
      input_files:
      - ../plain/half_2.i
      input_file_hashes:
        ../plain/half_2.i: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/half_2.i
    file_hash: 0b362a98d328467ff4a069dbed2be3429090ca070e60d49c76297e4bb94402b7
    line: 35
    column: 9
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
