- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fe925e9-133f-45cd-8125-5a42f36a3120
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 35
    column: 11
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a05e46a-97d2-41bf-a3e6-4576c324b52b
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 35
    column: 11
    function: main
  location_invariant:
    string: 1 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bd1455c-54fc-42df-81b0-f316ffc2417a
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 35
    column: 11
    function: main
  location_invariant:
    string: x <= 2147483645
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee406ab8-9bbe-4c4e-962f-267a54fa6250
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 35
    column: 11
    function: main
  location_invariant:
    string: y <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb0218f0-5535-401d-9d01-e8d583f85ca8
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 35
    column: 11
    function: main
  location_invariant:
    string: (-2LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2116e145-f4ef-4b7c-b999-95cbf2ad022c
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 35
    column: 11
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff1d54ac-31a9-4e12-8729-12f754543e66
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 35
    column: 11
    function: main
  location_invariant:
    string: y != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99556dff-9306-4234-8c2d-b727fd4c1abd
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 35
    column: 25
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27d662a4-e353-43d4-bae0-f611a849a974
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 35
    column: 25
    function: main
  location_invariant:
    string: x <= 2147483645
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f099d116-b6a8-40a3-b6bc-587914235645
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 35
    column: 25
    function: main
  location_invariant:
    string: (-2LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a20d50d-84b1-4251-a428-eead2915fd4b
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 35
    column: 25
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79912f04-2a20-4312-9d1a-4ac28c00fa12
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 41
    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: 4331c479-b526-445a-b118-ef86ec36b580
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 41
    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: 5e3783e6-a969-46de-9344-fa372c7a6b77
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 42
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13fe47dd-7121-4ae9-a912-7a4235f179f8
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 42
    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: 9f7781d0-ef06-4f29-aeb7-90784051d2bc
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 42
    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: 8d5bc152-14c5-456d-8c1d-471e1b9ccc55
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 42
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb69db24-c3d8-4e15-8a53-320d6f9eeef2
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 43
    column: 4
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a687439-c5ca-44ab-b0e2-dd95153c95a9
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 43
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6566e0b-1bd7-4eaf-b18a-60efec43e1a0
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 43
    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: 62112e31-b4f0-4a95-a02e-7a63279da17a
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 43
    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: 8718efa3-fb32-4413-9318-f5dee0a5748c
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 46
    column: 8
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 334e5c92-85e1-436e-832e-0f30aa471d2e
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 46
    column: 8
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2687b966-1f02-4966-b0db-c7953f69baef
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 46
    column: 8
    function: main
  location_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 412ac187-12de-4310-980a-c5d70e58ff8c
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 46
    column: 8
    function: main
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3a75c9e-c88f-4708-982e-51ffbf5162e5
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 46
    column: 8
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80186529-0135-416f-996b-81f86ecb3ee4
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 46
    column: 8
    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: 2ed692c7-2cb4-440e-a019-7a193391b736
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 46
    column: 8
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6df6b36e-1135-41a2-8ed8-13849dad2d9d
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 48
    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: a1961761-4c84-4319-9902-e0e6f00323e9
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 48
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8246185d-4598-413e-859d-3ef5f608d5af
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 48
    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: 6a9ec6d7-5b4d-4c23-88f7-098355eeb93a
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 48
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eafd4c29-1498-4443-9519-2a404c2760fb
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 50
    column: 4
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 703226c1-5b74-4c36-875b-c345c3c11961
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 50
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0bd54df-15b6-47ec-b1ec-fc40187d2d8d
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 50
    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: 6dc7462f-a9f5-4c7d-bc56-49dc1038ce7d
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 50
    column: 4
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de90da0f-0fa8-4b61-8973-e9325d906bdc
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 50
    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: 55c8a093-9ffb-413a-95c7-ce1666d5c239
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 50
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb10b6af-2a01-4d47-b52d-125e4cbbf282
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 19
    column: 4
    function: main
  location_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2f157de-435b-4666-8a34-88cef8707c60
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 19
    column: 4
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c6f74b50-0ad9-4cf4-8117-96d4dd006501
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 25
    column: 10
    function: main
  loop_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bdd36fb2-0cdf-496b-b246-34604d52a2c0
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 25
    column: 10
    function: main
  loop_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 381c63a7-ec27-4b36-9306-b2e8c8d7f097
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 25
    column: 10
    function: main
  loop_invariant:
    string: y <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 59dab378-dc38-4cdc-97b8-259613f67e61
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 25
    column: 10
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 346cdeca-6c2a-43e4-9485-c499f0d377ad
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 45
    column: 7
    function: main
  loop_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e640179e-070e-48d2-b830-58b84c050b86
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 45
    column: 7
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ed278eff-a041-47b3-8960-22d128ce9f5b
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 45
    column: 7
    function: main
  loop_invariant:
    string: x <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3692d5c7-e217-4017-b380-c8aaa3c4c029
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 45
    column: 7
    function: main
  loop_invariant:
    string: y <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e88814cb-bb5e-4dd7-b0b3-f64f6c87af02
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 45
    column: 7
    function: main
  loop_invariant:
    string: (1LL - (long long )n) + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d8a86902-05b5-4bd5-b109-4b2f05e18996
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 45
    column: 7
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5853d111-b039-472d-8da1-b2b27e350751
    creation_time: 2023-01-27T16:29:28Z
    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/elimination_max.c'''
    task:
      input_files:
      - ../plain/elimination_max.c
      input_file_hashes:
        ../plain/elimination_max.c: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/elimination_max.c
    file_hash: 0bc7b1b837bfd7794f122f6504da8d835bb2276ae4afe0cc0d058d385032d49e
    line: 45
    column: 7
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
