- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be851e44-73f1-4d62-9ede-5ed547e186d8
    creation_time: 2023-01-27T16:29:46Z
    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/phases_1-1.c'''
    task:
      input_files:
      - ../plain/phases_1-1.c
      input_file_hashes:
        ../plain/phases_1-1.c: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/phases_1-1.c
    file_hash: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
    line: 23
    column: 2
    function: main
  location_invariant:
    string: 268435455U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c943a7e2-036d-4465-af06-83ab54506570
    creation_time: 2023-01-27T16:29:46Z
    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/phases_1-1.c'''
    task:
      input_files:
      - ../plain/phases_1-1.c
      input_file_hashes:
        ../plain/phases_1-1.c: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/phases_1-1.c
    file_hash: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
    line: 23
    column: 2
    function: main
  location_invariant:
    string: x <= 268435456U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8bc16374-4ec8-46fe-804d-bdb3421e0152
    creation_time: 2023-01-27T16:29:46Z
    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/phases_1-1.c'''
    task:
      input_files:
      - ../plain/phases_1-1.c
      input_file_hashes:
        ../plain/phases_1-1.c: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/phases_1-1.c
    file_hash: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
    line: 23
    column: 2
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffc4a0bf-12e7-4a32-845a-d846d56b7924
    creation_time: 2023-01-27T16:29:46Z
    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/phases_1-1.c'''
    task:
      input_files:
      - ../plain/phases_1-1.c
      input_file_hashes:
        ../plain/phases_1-1.c: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/phases_1-1.c
    file_hash: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
    line: 16
    column: 8
    function: main
  location_invariant:
    string: x <= 268435454U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b8d38b1-b410-4b81-8cf3-fbf3d28a10f2
    creation_time: 2023-01-27T16:29:46Z
    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/phases_1-1.c'''
    task:
      input_files:
      - ../plain/phases_1-1.c
      input_file_hashes:
        ../plain/phases_1-1.c: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/phases_1-1.c
    file_hash: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
    line: 17
    column: 6
    function: main
  location_invariant:
    string: x <= 65519U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6caaf87-9b9d-4b0d-a4bf-0ec438fc746e
    creation_time: 2023-01-27T16:29:46Z
    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/phases_1-1.c'''
    task:
      input_files:
      - ../plain/phases_1-1.c
      input_file_hashes:
        ../plain/phases_1-1.c: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/phases_1-1.c
    file_hash: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
    line: 19
    column: 6
    function: main
  location_invariant:
    string: 65520U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d220721-67ad-44df-b6b4-7e7040bf6638
    creation_time: 2023-01-27T16:29:46Z
    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/phases_1-1.c'''
    task:
      input_files:
      - ../plain/phases_1-1.c
      input_file_hashes:
        ../plain/phases_1-1.c: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/phases_1-1.c
    file_hash: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
    line: 19
    column: 6
    function: main
  location_invariant:
    string: x <= 268435454U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1a9537c-7e7e-40fc-ac88-4acb0a61bc86
    creation_time: 2023-01-27T16:29:46Z
    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/phases_1-1.c'''
    task:
      input_files:
      - ../plain/phases_1-1.c
      input_file_hashes:
        ../plain/phases_1-1.c: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/phases_1-1.c
    file_hash: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
    line: 19
    column: 6
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 76388e6c-9972-438d-9b96-f814f479fb14
    creation_time: 2023-01-27T16:29:46Z
    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/phases_1-1.c'''
    task:
      input_files:
      - ../plain/phases_1-1.c
      input_file_hashes:
        ../plain/phases_1-1.c: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/phases_1-1.c
    file_hash: bc900b1bfcaecf91bc89637deaef4e1ddf2476faf43fa7e6f1e197c315ae3982
    line: 15
    column: 9
    function: main
  loop_invariant:
    string: x <= 268435456U
    type: assertion
    format: C
