- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0cb45e31-37c3-4d6b-9d55-be8ae8132c36
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 1 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2b82ba2-0858-4d4c-99d1-684b872554da
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 24
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4a3bca5-0ecd-47ad-8df2-1f64e38538f9
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 24
    column: 4
    function: main
  location_invariant:
    string: x != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff070841-d761-4d8b-bc80-dde2102c9e01
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c9825c55-0a74-4f18-8d34-8a61b916f374
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35888ac9-2e4b-4e37-951e-f73b11980b59
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 25
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73f53597-7304-49fd-b8d9-bbd040eb703f
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dfdada99-18a8-42b0-b927-989d4d09cf61
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 25
    column: 4
    function: main
  location_invariant:
    string: x != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94039875-c135-49f7-aa15-c5557fa8c481
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b910c7f-1b0e-407d-814f-1234adf1fd6d
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7bb72b4-d1b6-4a69-b957-a71496d862d1
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02296774-bf4d-4a2e-ac84-09c1060b7747
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: y <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc115c27-fe8d-4ad7-a244-6d5261e1281b
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37e33d85-e9a7-4544-8f0b-c81d0b1eda46
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: x != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb69a0eb-daf9-410a-8642-13df26f1ee80
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: y != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a304f99d-9b80-429d-bd4f-98fc08291a22
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28f68685-eabd-46f1-80ef-ad8c683f26ef
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7c61095-9c6b-4a55-9399-0908c5f44046
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5022f474-2a04-4cd3-b425-2664927617c3
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: y <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c61eb0a8-a473-4067-80ff-6c888a70e28c
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cd83122-85ae-4b68-832a-0c3def04d594
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: x != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 993ca744-d6af-4a12-bcf3-27a2e57078da
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 26
    column: 8
    function: main
  location_invariant:
    string: y != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 344b61a1-b5d4-4dbd-b26e-c7bbf6b80ab0
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 28
    column: 2
    function: main
  location_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f6006511-c59e-445b-9ce1-d89dfaea47e0
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 23
    column: 9
    function: main
  loop_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6429cadf-0b9c-46b7-ab35-ccee304433d9
    creation_time: 2023-01-27T16:29:17Z
    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/benchmark09_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark09_conjunctive.i
      input_file_hashes:
        ../plain/benchmark09_conjunctive.i: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark09_conjunctive.i
    file_hash: 64cd7ac5eb0a9d67f170f7116fe70bfc33ede6496f7f1decfe8a4115f59f37aa
    line: 23
    column: 9
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
