- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e9d5253-f386-451e-9f06-ff037e1e027b
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 29
    column: 8
    function: main
  location_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13f2f8fd-ef86-4717-bbc7-9d53c85a84b4
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 29
    column: 8
    function: main
  location_invariant:
    string: n <= 1000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9194dbe5-3620-494d-88c8-d811ed5e8548
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 29
    column: 8
    function: main
  location_invariant:
    string: 1000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c54f3f59-f845-4c61-abdd-7f15d4916e08
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 29
    column: 8
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9458b0cf-80fb-4af9-8baf-9d6cbb8cbfd6
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 32
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4575cc14-fcb6-4ee5-8106-918c05600c2b
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 32
    function: main
  location_invariant:
    string: i <= 999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca5f2a96-56f8-4098-b774-3b5c80e8694e
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 32
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f390bd9c-db8a-4172-ae59-bfa8e6ba3471
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 32
    function: main
  location_invariant:
    string: 1000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 685535a6-4290-4946-82eb-ea23ccfa6415
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 32
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fffe7956-5399-4147-ac63-a8b225db1466
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 32
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06526783-06bf-42e1-8ed8-b25f7d7aaaac
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 32
    function: main
  location_invariant:
    string: i <= 999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9738d86-6853-4625-be02-b6f884af9380
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 32
    function: main
  location_invariant:
    string: 1000LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e1d63b8-4fb1-49a0-bc1d-96f33c96e534
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 32
    function: main
  location_invariant:
    string: (-1LL + (long long )i) - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ede286dc-c7dd-4ce5-aaa3-6376461e2d2f
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 32
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fec0a2bf-4d7b-4c1a-8520-104bbf7c9cd4
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 1000LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 006ef9c1-7f75-4d52-8d03-37c41e3570fc
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    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: 61dba821-4e1e-4668-940d-5067de1260a8
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d0cfc8f-ca85-4b09-addd-8e7f829e73d3
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 28
    column: 8
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75115eaa-f8ed-4e1d-a8a9-704b045121ae
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 28
    column: 32
    function: main
  location_invariant:
    string: -1001LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d8a1897-2517-4a23-bfb3-c80a705ed85b
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 28
    column: 32
    function: main
  location_invariant:
    string: -1LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 132ef254-143c-4510-a9b1-23c145eb5f25
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 8
    function: main
  loop_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b926808a-74b8-40a7-9c58-289e80b17bcb
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 8
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c70a3fe-43fc-475b-9450-d45092ff035f
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 8
    function: main
  loop_invariant:
    string: n <= 1000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 70c54711-5cad-464d-a8e8-1b001a2570b7
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 8
    function: main
  loop_invariant:
    string: i <= 1000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 58b6e137-d93b-409a-a99c-5197ef8e7433
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 8
    function: main
  loop_invariant:
    string: (0LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 186f9cfe-d793-45af-af45-277d72458c44
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 8
    function: main
  loop_invariant:
    string: 1000LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e6c960da-ad67-48a8-a217-73d3cf582742
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 30
    column: 8
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c80002e3-749e-49ec-8581-081c373bfe28
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e6d702f6-3a29-431d-b521-8bd4d272c065
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 77701125-be35-4e1a-af05-1e96ec6c3fc8
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c9419ada-dbf8-4173-808c-04ab0cb0624b
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: n <= 1000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8261bb76-83d8-4502-ae89-b7858b12ca97
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: i <= 1000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c6bf778-3e19-4583-a406-902c9824519b
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: i <= 1000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7eb2a4c5-44fe-4d34-9ec5-723614081e96
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: 1000LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7deeddf8-33b0-4d4f-ab23-45383bb03e8a
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: (long long )i - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 131c3cae-494d-47b3-875a-87b1f4ac0820
    creation_time: 2023-01-27T16:29:43Z
    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/mcmillan2006.i'''
    task:
      input_files:
      - ../plain/mcmillan2006.i
      input_file_hashes:
        ../plain/mcmillan2006.i: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mcmillan2006.i
    file_hash: 45cd9f1eda35cecb580d3b7fe5199506be9e5041f2297c1c3e22e0a862fa68be
    line: 31
    column: 8
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
