- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 445d5e3f-a57a-4d0a-b0ab-c511932b6f0a
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 21
    column: 2
    function: main
  location_invariant:
    string: x <= 65536U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e17236ae-aac4-4ee3-918b-6ada9e959898
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 21
    column: 2
    function: main
  location_invariant:
    string: (0LL - (long long )N) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f2645d00-509b-471a-8859-733e003c3a12
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 21
    column: 2
    function: main
  location_invariant:
    string: 65535LL - (long long )N >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27148b3f-8f3f-45dc-ac21-e75ae76fff2b
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 21
    column: 2
    function: main
  location_invariant:
    string: 2LL * (long long )N - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1ad8afc-e10e-42a3-81c1-d112c4271ea5
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 22
    column: 0
    function: main
  location_invariant:
    string: (0LL - (long long )N) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c58ec7a2-b2ab-4746-86b2-39b8c27a3333
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 22
    column: 0
    function: main
  location_invariant:
    string: 65535LL - (long long )N >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 96bb2740-2c2c-4ff3-9621-605fe53fcb82
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 22
    column: 0
    function: main
  location_invariant:
    string: 2LL * (long long )N - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a9647b3-b63b-4c79-a754-dfcc6fec91f7
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 65535LL - (long long )N >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c342594-3b59-429f-ba64-f12301d53937
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffb52cfc-fdae-4a6b-8ce1-a86c8048fa0c
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fedd8abf-4cac-4bba-a36f-b9332fb8e3ee
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )N >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75020bee-3342-4ab4-985d-714c456523cd
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 15
    column: 17
    function: main
  location_invariant:
    string: 65535LL - (long long )N >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27a65537-66ec-482b-b0b8-96cbc0f5fe7d
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 15
    column: 17
    function: main
  location_invariant:
    string: (long long )N >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6e74e25-e6e2-40d1-a40f-afa4541b0082
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 18
    column: 4
    function: main
  location_invariant:
    string: x <= 65534U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca0b07c9-c364-415e-bf5d-40fb4b61212d
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 18
    column: 4
    function: main
  location_invariant:
    string: 65535LL - (long long )N >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2fe51bec-973b-4a9f-bcbf-807ca5d08125
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 18
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )N) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd9b6baf-9036-4504-81ff-e57632346162
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 18
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 76aac2c4-2e37-4ee6-9055-a2f642b127c8
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 17
    column: 9
    function: main
  loop_invariant:
    string: x <= 65536U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3963b8e4-5c91-40a1-90ba-cb0128834cb8
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 17
    column: 9
    function: main
  loop_invariant:
    string: 65535LL - (long long )N >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 90b29263-23a8-46a7-ab4a-d4071184ca8b
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 17
    column: 9
    function: main
  loop_invariant:
    string: 2LL * (long long )N - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eb3728ab-09b6-4936-8ea5-0dd2dd88f558
    creation_time: 2023-01-27T16:31:03Z
    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/simple_3-2.c'''
    task:
      input_files:
      - ../plain/simple_3-2.c
      input_file_hashes:
        ../plain/simple_3-2.c: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/simple_3-2.c
    file_hash: 8b9c8396c2cadaebd0d1bf5efb2e2e779b8a2240a5737f65c06e64ea585aef3c
    line: 17
    column: 9
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
