- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a74797be-ca03-4718-a76b-e29845ec3f94
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 22
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3cc0d15-1718-414d-9505-34227bacb317
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a469d3c-3a8b-4a93-822a-5e6154ba6f9e
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 27
    column: 8
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6c57eca-b351-46b6-b261-1b2421b78703
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 27
    column: 8
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 065ab58b-6534-461f-8ad7-9405e164c260
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 27
    column: 8
    function: main
  location_invariant:
    string: i <= 4
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd02f6b5-081e-4a18-a4bb-dfeb842c7a4a
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 27
    column: 8
    function: main
  location_invariant:
    string: j <= 5
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0f52aaa-93ec-4d89-a9f4-0c3fb53cc7da
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 27
    column: 8
    function: main
  location_invariant:
    string: 4LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d562d9b9-70a6-4298-98d2-fd820fe04a35
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 27
    column: 8
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 371af04f-3063-4fa0-bf40-08c50029a483
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35450a8f-ad21-491e-8267-a1adb3c02e86
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 28
    column: 8
    function: main
  location_invariant:
    string: j <= 5
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 777124f7-c1c1-4916-b473-000a52987412
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 28
    column: 8
    function: main
  location_invariant:
    string: 4LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77a870aa-cdf9-4fc0-a273-00a500cc1419
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 28
    column: 8
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 671731f5-0c43-40f1-a398-20ac6fb9efcc
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 31
    column: 4
    function: main
  location_invariant:
    string: -1LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb208e0e-9d64-434b-859b-041027b8e6ad
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 33
    column: 6
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43fbad00-ce41-43fe-a191-7ed761bf6104
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 33
    column: 6
    function: main
  location_invariant:
    string: j <= 4
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bddda7bd-aa3e-4ca9-a384-b63048067714
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 33
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2789a51f-7a42-4801-be7d-a1fbf72c819c
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 34
    column: 6
    function: main
  location_invariant:
    string: j <= 4
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b084423-3c5d-4447-99c2-06e3283d66db
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 34
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed7b031f-88d7-4a89-a9df-4086a800f7a4
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 36
    column: 0
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20e7d823-51f1-49cd-a2dd-6c149c2dc3aa
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 14
    column: 17
    function: main
  location_invariant:
    string: 4294967295LL - (long long )max >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0cf316c6-a8cf-4a1f-9535-e3a7453f09e8
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 14
    column: 17
    function: main
  location_invariant:
    string: (long long )max >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c97550b8-9f69-48c9-a01d-3fc3d64e995a
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 19
    column: 8
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3bc0ae4-569f-42f0-9aed-42ae7d6d0c11
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 19
    column: 8
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fcb3ec58-1587-4a03-a7d5-7d0132c0d3f5
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 26
    column: 8
    function: main
  loop_invariant:
    string: -1 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 44fc4a0c-1968-4668-bf23-dc9e06f96b56
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 26
    column: 8
    function: main
  loop_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4aa09629-b51a-4f11-bbe3-6f923f2c7aa0
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 26
    column: 8
    function: main
  loop_invariant:
    string: i <= 4
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d8852b7-9d55-487e-9e2d-86477de9215a
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 26
    column: 8
    function: main
  loop_invariant:
    string: j <= 5
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f7114cc-ef92-45d6-871c-0bbc156c6273
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 26
    column: 8
    function: main
  loop_invariant:
    string: 4LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e7626304-f967-452f-8b19-a6de16801659
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 32
    column: 8
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 088d5afe-3bc4-4ff5-a3f4-c7927d7ee1d6
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 32
    column: 8
    function: main
  loop_invariant:
    string: j <= 4
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f8dcfe73-4d3c-42e8-a8f6-d482bf097cb1
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 32
    column: 8
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 85492425-4966-4c3e-b4ea-fdc328af9827
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 18
    column: 8
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4916aa29-28bc-4190-b8bb-943f04d5d6d7
    creation_time: 2023-01-27T16:29:40Z
    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/invert_string-3.c'''
    task:
      input_files:
      - ../plain/invert_string-3.c
      input_file_hashes:
        ../plain/invert_string-3.c: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/invert_string-3.c
    file_hash: ca98535e808a51f7cfa7d21c9d33f259821212a6554e27f29c2bddd9197c0249
    line: 18
    column: 8
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
