- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24d0ba42-2527-4d8f-b64d-5180da45fd52
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 23
    column: 43
    function: main
  location_invariant:
    string: -101LL + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b672d3ea-3b73-464e-8621-b31812519e05
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 23
    column: 43
    function: main
  location_invariant:
    string: -1LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77303b06-6747-417f-ac20-7f7ed85d5de7
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c77ac17-0021-4573-a805-064133499541
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 0 <= sum
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 173a0c0e-6e27-4170-944c-b086221f14c5
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 25
    column: 4
    function: main
  location_invariant:
    string: i <= 99
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db078acd-c53a-457e-b976-264550449ae7
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4efebd5-6547-462c-9160-b4daa6a1848a
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 100LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef960bff-ea4d-4562-bed2-f7c14e0cff86
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a0660c5-828e-4552-b892-e825407390e8
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 0 <= sum
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f429b17b-0e6d-4c94-9323-1f3951c5f2d7
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 26
    column: 4
    function: main
  location_invariant:
    string: i <= 99
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b4771f1-dc8b-4fbb-af0a-ee47afccd184
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39957737-2db1-4961-bb13-8c04516c41a3
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 100LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 515ae9cd-2b5f-4a22-8c87-fa4272056bac
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 28
    column: 2
    function: main
  location_invariant:
    string: 0 <= sum
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e9ba8ef5-fd52-4068-910b-cdd4aa551536
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 28
    column: 2
    function: main
  location_invariant:
    string: 100LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92fe913f-0681-452c-bd88-94a7c531b081
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 29
    column: 2
    function: main
  location_invariant:
    string: 100LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d229b02-98d8-4cf5-b15a-1d24463e4316
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 23
    column: 6
    function: main
  location_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfdf044a-0dac-4553-9853-b2ff5a32dd96
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 23
    column: 6
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9674be0f-fbbe-465b-bb8d-6521ba2d9edb
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 23
    column: 6
    function: main
  location_invariant:
    string: 100LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 393a2a3e-4537-414a-89fe-56f5d50641f9
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 23
    column: 6
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8db2e2b8-3d1d-4643-a990-3b884b406a93
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 23
    column: 43
    function: main
  location_invariant:
    string: 100LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f65f7607-0dff-4ddc-a829-a065d959979d
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 23
    column: 43
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1bc9269b-ff26-42ae-9ca2-c6360aeaf8ca
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cabf9e2-0cb6-4bc6-a120-3859a41e41fe
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: 0 <= n
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 39f1cb5e-a01d-4a33-9382-b9b0ff6a8266
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: 0 <= sum
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 97964e26-387d-459e-9350-0429a9ac030c
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: i <= 100
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c3f77cc2-b863-4aea-b3c5-b1fa556d3ccd
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: n <= 100
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 06b67f0a-f84e-40f4-af67-1c1770dec1ef
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: (0LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d7db173-d6d2-4efa-ba52-d994fdf805a1
    creation_time: 2023-01-27T16:29:18Z
    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/benchmark20_conjunctive.i'''
    task:
      input_files:
      - ../plain/benchmark20_conjunctive.i
      input_file_hashes:
        ../plain/benchmark20_conjunctive.i: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/benchmark20_conjunctive.i
    file_hash: a97cc7ecf3f325d6a4f94ad142da468f60264f8646a5f445527873ff4eb9457a
    line: 24
    column: 9
    function: main
  loop_invariant:
    string: 100LL - (long long )n >= 0LL
    type: assertion
    format: C
