- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 082602ff-f906-4b13-bf91-a3aa1cac76a4
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 33
    column: 8
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0a08749-9abd-4de4-84a8-aa73004b11c3
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 33
    column: 8
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d9b0505-289f-429d-9f6f-2ccf8bd248a1
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 34
    column: 12
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21e42ca1-b5cc-4918-abdb-c110ae57b33f
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 34
    column: 12
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7331276a-df41-48ea-8a85-47d96076507d
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 37
    column: 12
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: decd1007-71e4-49a9-8371-c813b7e6d6d5
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 37
    column: 12
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc3e1353-0a74-48f4-9c8f-69f7fbe92227
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 37
    column: 12
    function: main
  location_invariant:
    string: y != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32c299e0-0c11-45d6-8973-3f8ef76ca182
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 39
    column: 12
    function: main
  location_invariant:
    string: -2147483647LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19bfa020-5139-4bca-a84a-0eef8175dd0e
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 39
    column: 12
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4aa4ed9c-648c-4373-a302-fe2c111ac6a8
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 39
    column: 12
    function: main
  location_invariant:
    string: y != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ab14f3d-faea-4fdf-a438-cba46400b226
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 41
    column: 8
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5da356d0-c717-4413-8902-884b8e747d5b
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 41
    column: 8
    function: main
  location_invariant:
    string: y <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4766733-d9d0-4039-adb3-1e7290b416bf
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 42
    column: 8
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27c24c46-ea38-4872-b47c-3db0ff11da98
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 42
    column: 8
    function: main
  location_invariant:
    string: y <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8662bc6-746d-402d-b62c-fbd5f865a2c1
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b401db0-832f-418b-adea-d33563746c8e
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 29
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98769d0d-2234-4fe5-836b-b3dfefb1663a
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 776509a4-adca-42ca-9057-810cfe716eb5
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 30
    column: 4
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ad1de59e-8378-4b05-ba4d-10bcaa8b2813
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 207ecc4c-1386-4f24-9035-476cfeb2750e
    creation_time: 2023-01-27T16:29:46Z
    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/prodbin-ll.c'''
    task:
      input_files:
      - ../plain/prodbin-ll.c
      input_file_hashes:
        ../plain/prodbin-ll.c: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/prodbin-ll.c
    file_hash: 77bbfba272f7904e5efe099569a5ed86d54de3fd07a8ce9d48301467c5048e30
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
