- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b72cfef0-ce73-4813-8048-5caf5dfb4778
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 29
    column: 8
    function: main
  location_invariant:
    string: 1000000LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac6e2655-64e9-461d-ba2b-629dc652c7e4
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 29
    column: 8
    function: main
  location_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0170404-a439-487f-aef7-8d38afe233b7
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 29
    column: 8
    function: main
  location_invariant:
    string: 1000000LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f4d2e72-7e7f-4c7d-8834-e1654c0c32b8
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 29
    column: 8
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 223fe2c5-ce32-490a-9ed3-33b323e58f5f
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 29
    column: 35
    function: main
  location_invariant:
    string: -1000001LL + (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5de1448-8f80-44d1-9c36-cb0c6ff8e9a9
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 29
    column: 35
    function: main
  location_invariant:
    string: 1000000LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b918d35c-3c23-4c31-aad2-527e32e8247b
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 29
    column: 35
    function: main
  location_invariant:
    string: -1LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 659f3435-f325-4a1f-8655-6c4a61c84e59
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 29
    column: 35
    function: main
  location_invariant:
    string: 1000000LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29f71cf7-476f-47ea-a5e2-34a737e4d96a
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 30
    column: 4
    function: main
  location_invariant:
    string: a <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e8c3d97-93d2-416b-915e-ec619f9e8d1f
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5af832dd-02e5-4f91-ad76-fe916f37827c
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 30
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 308c2aa1-ad88-4b5b-84d7-dc8994c667e7
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93180107-7dbc-4e5c-8667-85b298a55217
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e937e7d-436e-469d-b8ea-b344044f7e18
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 31
    column: 4
    function: main
  location_invariant:
    string: b <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bba60a8d-759c-4970-a07c-50572f41ccef
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 31
    column: 4
    function: main
  location_invariant:
    string: res <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08aa0a07-5b70-4c9c-a066-060d82d1f9fe
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39fe33a4-87b3-49bc-bc39-b0a4e5f68019
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2495668a-c84d-48c5-957f-dbd509c5ac0f
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e186dac3-0b27-4423-b5d2-28afc84df4f1
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 33
    column: 1
    function: main
  location_invariant:
    string: 1 <= cnt
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 910efa0a-dbed-4975-9b26-a34e22981a6f
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 33
    column: 1
    function: main
  location_invariant:
    string: cnt <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ada40652-3add-4ff0-abd3-88ea1befe64e
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 33
    column: 1
    function: main
  location_invariant:
    string: -1LL + (long long )cnt >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ce8ddda-acef-4a8e-aad1-6e1cd63dacfe
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 33
    column: 1
    function: main
  location_invariant:
    string: 1000000LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 378bf5ed-abbc-43fd-be5e-9048ce761fcd
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 33
    column: 1
    function: main
  location_invariant:
    string: 1000000LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e321334-1223-41e9-ae2f-d36818811f21
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 33
    column: 1
    function: main
  location_invariant:
    string: (long long )b - (long long )cnt >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bba2bf47-ca48-4d44-9cf6-da67d6772ee1
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 33
    column: 1
    function: main
  location_invariant:
    string: cnt != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98988c12-8496-476a-ba57-3ec255e40f12
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 34
    column: 1
    function: main
  location_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f1982c6-ff76-42de-9fa0-e307565ad51a
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 34
    column: 1
    function: main
  location_invariant:
    string: 0 <= cnt
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b4d94c4-6f91-4a7c-97e6-9f40b765b3ef
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 34
    column: 1
    function: main
  location_invariant:
    string: b <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e993cbd5-5343-4abc-992b-98cf6855e9dd
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 34
    column: 1
    function: main
  location_invariant:
    string: res <= 2000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 195477ef-3d3a-4d6d-96e4-4b9bf820520a
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 34
    column: 1
    function: main
  location_invariant:
    string: cnt <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be2f9cc1-7dad-46bf-88f0-eba018737145
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 34
    column: 1
    function: main
  location_invariant:
    string: 1000000LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec851de5-d269-4af7-a357-1f4b732dbda4
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 34
    column: 1
    function: main
  location_invariant:
    string: 1000000LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13fa2006-c671-4661-8cd1-e5fb7621c254
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 34
    column: 1
    function: main
  location_invariant:
    string: (-1LL + (long long )b) - (long long )cnt >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ca6af07-f950-46a6-89ce-21c8b4164d84
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 34
    column: 1
    function: main
  location_invariant:
    string: (long long )cnt >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd21630d-a6ee-42d3-9983-16304419cf89
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 34
    column: 1
    function: main
  location_invariant:
    string: cnt != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e80776a-1ec0-4939-8a34-15e9bac3cbd9
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7a28fc7-b332-4538-b0d5-eb8946d0af2a
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 36
    column: 4
    function: main
  location_invariant:
    string: a <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 935e71c3-8594-45b6-9a73-4d0eae79168e
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 36
    column: 4
    function: main
  location_invariant:
    string: b <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cff1d8d4-69b2-4c7d-8eac-11ac884ba666
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 36
    column: 4
    function: main
  location_invariant:
    string: res <= 2000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bbe88acc-f9f2-49b7-af24-e96f3777c092
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64d879c6-5f9d-4773-998a-3a627c37784e
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7fb99378-fe24-4625-920f-acda4c886300
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c85f55cf-75f9-49ad-b80b-527a481941eb
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c924d7b0-24e3-482a-9257-7aa0ea6ed302
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 1000000LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 293497db-ea29-4476-a538-d4556128ff0c
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 37
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7688d4c7-8e79-44ab-837d-09f0680238c1
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 28
    column: 25
    function: main
  location_invariant:
    string: -1000001LL + (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 411346d2-f639-4302-b194-b26245fe3a56
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 38f1ab4c-6dc6-4f98-a7d3-10aa557c8877
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: 0 <= cnt
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ed5e2489-e5e9-4e8a-84e9-46bcb9cb8bd6
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: a <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 02ddeda3-8e89-422a-b6d1-f4e8dfc54f51
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: b <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 76ebc301-2e8a-497b-a40f-13da6f4b16f4
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: res <= 2000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 67e5c74b-e871-4546-8d19-b40efa406bb7
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: cnt <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a27a02a4-116b-48fe-b505-e6dee03ad445
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: 1000000LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 06b6c413-67a5-40fd-b878-18131c2afd40
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: 1000000LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b9c1591-8307-4fac-a13c-6448d4b596bc
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: (long long )b - (long long )cnt >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b90a98c3-c717-4707-98c7-5d6c321dd7ec
    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/hhk2008.i'''
    task:
      input_files:
      - ../plain/hhk2008.i
      input_file_hashes:
        ../plain/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/hhk2008.i
    file_hash: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: (long long )cnt >= 0LL
    type: assertion
    format: C
