- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 240676e6-5694-4467-9e73-8f2e3e26396c
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 23
    column: 7
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf1ec825-d192-4386-9cc8-7c13200b694e
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 23
    column: 7
    function: main
  location_invariant:
    string: 1 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37313942-30de-4e22-a1b4-5158958a59f9
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 23
    column: 7
    function: main
  location_invariant:
    string: x <= 2
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eabf406f-d8f6-445e-86ce-817363dfe5f7
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 23
    column: 7
    function: main
  location_invariant:
    string: x <= 127
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8207653b-dbd6-4818-9f88-ebe43d9e7f17
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 23
    column: 7
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63fb8ae8-0d52-456a-b5b5-1764aebf1d2f
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 23
    column: 7
    function: main
  location_invariant:
    string: 2LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9d7c905-a105-49f2-aa48-1131a4edcd85
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 23
    column: 7
    function: main
  location_invariant:
    string: x != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3cce89d7-4663-47c9-aa1d-e2bf1398b223
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 26
    column: 2
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69055ab3-f621-49ec-944c-701ec6c764d5
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 26
    column: 2
    function: main
  location_invariant:
    string: 1 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3175b0f4-07e5-482b-a57f-037c5d174c1b
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 26
    column: 2
    function: main
  location_invariant:
    string: x <= 2
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5316b81-25f4-466d-9192-67668f547235
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 26
    column: 2
    function: main
  location_invariant:
    string: x <= 127
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb1d7a5f-521f-4950-a381-e199f33d9e1a
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 26
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c74d60fd-a85c-4b8d-8569-8210691c9cf2
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 26
    column: 2
    function: main
  location_invariant:
    string: 2LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5b63489-fe67-4909-b8fb-b41ab36c100d
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 26
    column: 2
    function: main
  location_invariant:
    string: x != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94e3add6-dd50-4b10-9fc5-a359b04f00be
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 27
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eedc2270-5087-470b-8890-d013bda1ef74
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 27
    column: 2
    function: main
  location_invariant:
    string: 2LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad16c0bf-3fbd-4af1-9cda-0bcd402775be
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 21
    column: 6
    function: main
  location_invariant:
    string: x != 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 440dc9cc-be7f-4346-a39b-307125cf6c79
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 22
    column: 9
    function: main
  loop_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bfe8c0a3-94c3-47d9-86c6-3e467d1acf8c
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 22
    column: 9
    function: main
  loop_invariant:
    string: 1 <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 16f884b4-ad56-446f-ad4b-d81ec17c9688
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 22
    column: 9
    function: main
  loop_invariant:
    string: x <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 46825474-eb92-430f-905d-548322bbb2cb
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 22
    column: 9
    function: main
  loop_invariant:
    string: x <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d7efb980-0217-4ad5-a8e2-ee861f257ef2
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 22
    column: 9
    function: main
  loop_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ad9295f0-68df-4800-aec1-9e73ce49635b
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 22
    column: 9
    function: main
  loop_invariant:
    string: 2LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 440c4d34-b625-475b-b928-0258044d0018
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark32_linear.i'''
    task:
      input_files:
      - ../plain/benchmark32_linear.i
      input_file_hashes:
        ../plain/benchmark32_linear.i: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark32_linear.i
    file_hash: 8731c7b889cdaf4eec07de8973e6494ef97dd5e8bf9fb9fde3d7808725d4f0de
    line: 22
    column: 9
    function: main
  loop_invariant:
    string: x != 0
    type: assertion
    format: C
