- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f43be93a-6abe-47b1-8805-5ba5b52a6e15
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 19
    column: 9
    function: main
  location_invariant:
    string: x <= 98U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad4f26b5-1c02-4efd-bfb4-442f39eaf450
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 19
    column: 9
    function: main
  location_invariant:
    string: 98LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6c6d5ed-57c7-4527-a21f-233bfcee66f9
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 21
    column: 8
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 894f8658-0d12-4779-88d2-7446c0f99f8e
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 21
    column: 8
    function: main
  location_invariant:
    string: x <= 100U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29b9bd78-b055-4dde-a6e9-5f8d9a25d573
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 21
    column: 20
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5d09de2-e05b-441a-8005-170f0f90aa82
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 21
    column: 20
    function: main
  location_invariant:
    string: x <= 100U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54e3800f-b6ab-4604-96b1-792785b58e35
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 22
    column: 9
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d07c5c3a-5db2-43e0-8213-4d883a04d0f0
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 22
    column: 9
    function: main
  location_invariant:
    string: x <= 100U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7ccab42-3a6b-4c87-829e-fbf65c7733f7
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 49
    column: 2
    function: main
  location_invariant:
    string: 99U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 888dc88a-9d8c-4ce2-a694-9d4e3c783394
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 49
    column: 2
    function: main
  location_invariant:
    string: -99LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de22864a-3554-42e7-a558-b1be08c4302c
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 49
    column: 2
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cfaff9de-3a5c-4a97-9ce6-b6ccba417324
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 50
    column: 0
    function: main
  location_invariant:
    string: -99LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5cd24e0e-0083-49f1-956a-f039ea630ed6
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    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: 4bfc0cbf-d423-4d70-857c-d50b103c0034
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64405d3a-dabd-48bf-a40c-e0e05ef58beb
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    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: 5fb065ee-3d1e-4c57-8287-ec802fc32cb0
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7642ac6-03e2-4064-a23a-6b066841728b
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 790fded3-65a5-4aed-80eb-d5cb6b6c5af0
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36a1d187-2f01-4eef-9b13-d076a5f411db
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 18
    column: 8
    function: main
  location_invariant:
    string: 98LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fda24797-3678-4445-b073-1f68d94c3507
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 18
    column: 20
    function: main
  location_invariant:
    string: x <= 98U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87c1bce8-dde9-482b-8f6f-5b1d49580af3
    creation_time: 2023-01-27T16:29:22Z
    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/diamond_2-2.c'''
    task:
      input_files:
      - ../plain/diamond_2-2.c
      input_file_hashes:
        ../plain/diamond_2-2.c: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/diamond_2-2.c
    file_hash: 5b285e679a61ee5ec3c0d899a4a7682d4249c0885f5b4a5875891b312f202de4
    line: 18
    column: 20
    function: main
  location_invariant:
    string: 98LL - (long long )x >= 0LL
    type: assertion
    format: C
