- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a05c2fda-0fa1-438e-944f-9dc927d669df
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 22
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af2d8e66-d897-49c7-9f2b-8a9c3636aa30
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 22
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e703d6d9-e412-4c19-afc1-81c228b2c193
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 22
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f860ce2b-3307-402e-8f41-737048b67bc5
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 22
    column: 2
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be1caf13-59e6-42f9-9107-917134cba6fb
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6e00871-feca-4cbc-b623-af0b3a71eaed
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 25
    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: b3923a96-18ec-43be-bc2d-c00ba2597fae
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3af5c659-e4ca-45ba-8626-886f81125323
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 550c9c32-070d-40c9-9b99-d112d28a701a
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 1U <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fe90224-0e75-48e9-87b2-d9ad6a7f2e75
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 26
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99b805ae-79e6-420f-bb20-971deaad77b2
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62588279-f0a9-4ef5-914d-68974b857119
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a41bbe2d-6bd2-4c5e-a344-764164f6bfd2
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 26
    column: 4
    function: main
  location_invariant:
    string: z != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 66b28d01-dad9-4367-85a5-4c974f3a4615
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 31
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f84ac90-3fa3-4a5b-af48-802de2877997
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e3755b9-42e9-4215-ba16-0658e7a46b66
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9559b08-b7d0-4755-a99d-95195a0801d8
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 1U <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 294548f9-706e-4c19-8b1e-6a03f0c100fa
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 32
    column: 4
    function: main
  location_invariant:
    string: x <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa0e6cf7-ff88-4ce6-8391-5ad5c5888387
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 17df6188-b99a-4fc5-9f73-ab7277d7136a
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 32
    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: e5fef66f-9221-457a-82f2-7c17b3ff4f57
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0550a7e5-b03b-4dcb-8e62-802e00b4c399
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 32
    column: 4
    function: main
  location_invariant:
    string: y != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1be5467-4645-4205-b905-39efe81a7973
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 35
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8f39b5c-b01a-4848-8fb5-e4758260bfc2
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 35
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71accaaa-e845-4e5c-a1a5-d57be1941ddb
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 36
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc0b81a4-1e05-4dd4-bf01-1bf45533e10e
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 36
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36a13595-41e0-4077-afa8-27d4d9217919
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3fadb520-0778-4f26-b64e-d1d1bc8841d8
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    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: f7defad0-2fc3-4883-8d64-af13f5faf3e2
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    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: 388219a1-f324-4943-bb42-75277b6d010a
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5a1e900-6665-4874-8d5c-f1ca1cad974b
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    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: 08da7331-9ea2-401f-9f11-82f2b41a35ad
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    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: ef5e2019-5271-4661-bfa4-60a6a8dbb173
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    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: 78d826a5-f3fa-4239-b80c-b11337ec3a30
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffcb2d37-8f15-411f-b8e5-a7f9e60fc1b7
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 608f22f5-6a5f-4aed-aa98-fac2230a2b56
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    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: aa15b66f-c0ee-42cb-8767-805ab224bd2b
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    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: c1ecaa95-1b54-4191-8f46-caefeaa35cce
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c5a032e-6698-4c56-bda0-423861e9fb80
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    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: 9c52cf3c-08ea-4b2a-a058-aa5201ac071a
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    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: 78b24fa4-bf52-4f95-acd1-8a5460150cf1
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    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: 88596c64-f587-4f67-88c7-50b4b5a7466f
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b305ecb-b358-417f-82d1-70c61c9b8f5f
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae8a46db-3e1c-4713-80c0-b450efa5a25e
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c5a61318-4efe-4453-b572-4964d72e6591
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef4c9bcb-e1e4-4f3f-84ed-911d3fba2fb9
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    column: 20
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6aa96660-1daf-459c-8a58-4d55f59474b6
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    column: 20
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae06fb06-1a5b-412c-975d-08aa797571e1
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 15
    column: 20
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 175c2ac0-4bb2-4861-81fa-227bbc1406eb
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 18
    column: 4
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4b975de-f0de-4923-a4df-5e51219e4570
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 18
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25b147fe-aefd-4752-85a6-a8a773f566f1
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 18
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca436f9a-0cee-414e-9cb3-6f994da72d30
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 18
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6129bcd-9eee-40c3-bde4-ff520ef5a864
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 18
    column: 4
    function: main
  location_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ace65d81-ba53-4b84-a3eb-cbf679a340d9
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 18
    column: 4
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 216c14df-9a46-43d3-a90b-67b2e9c82f1b
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 18
    column: 4
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1919bfe-0774-4a27-af63-289bb68dccb2
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 19
    column: 4
    function: main
  location_invariant:
    string: x <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bbdae01-932c-4c3b-ac9c-8f59e562d32c
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 19
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c89ad944-611e-4d33-9c65-3b9ba8040604
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 19
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d736fadc-2cf6-45f4-b7fb-f67a5e75c5ef
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 19
    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: b9c03e80-3210-44e2-bcb4-76f2a7e00565
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 19
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36935de3-5cf3-4c10-977a-a52a2d05fc59
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 19
    column: 4
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62ccd4be-4099-464e-b0ae-1ccdd61d02a8
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 19
    column: 4
    function: main
  location_invariant:
    string: x != 4294967295U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9df62ccd-c99c-4341-b846-9cc4e9369415
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 973fbfa5-39c8-4521-ab46-1e887330410d
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a7ea0473-f14d-4371-8918-c2e2759ad037
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e55bd77f-5b85-4b47-ad3e-77959e3f16c3
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cbf6c621-9bd1-4d13-acc0-1ba53033f2df
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f178b71-5f01-40eb-83dc-2892937fa403
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c442daef-574b-4e0a-bf2f-d8deeea0d0ed
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 604c5c65-6cb5-4394-ad35-bf87a4935763
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eecd5729-1d15-456f-afa6-c465c0a2e6da
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ffcabae2-b8ca-459a-b3d5-2a786b7c82f8
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 798f4280-3760-4877-8d49-eee79639b7d8
    creation_time: 2023-01-27T16:29:39Z
    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/in-de32.c'''
    task:
      input_files:
      - ../plain/in-de32.c
      input_file_hashes:
        ../plain/in-de32.c: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de32.c
    file_hash: be02771c62bfe2ce14e3e1aa527948281d29318788bbe261fd0d537b1dc5e291
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
