- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56c168e8-46af-431d-a01c-4dca4acd30fd
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 25
    column: 2
    function: main
  location_invariant:
    string: -10LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec727d8b-cb07-489d-93b1-a031b21ba777
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 25
    column: 2
    function: main
  location_invariant:
    string: 255LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2302f79-180b-4382-a77e-15542e54062c
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 25
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 240f2442-2298-42ee-8bd4-ff23052901c0
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 25
    column: 2
    function: main
  location_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c063c760-384e-497a-9572-dff9f537e710
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 25
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 360c9e57-737d-4984-93c4-be672cbd8120
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 26
    column: 2
    function: main
  location_invariant:
    string: -10LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4262ee98-82ca-46a8-be98-fcf6c08032f4
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 26
    column: 2
    function: main
  location_invariant:
    string: 255LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: deb7e4d8-78a5-4a1a-bfec-3cb2668d3492
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 26
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6d587e7-ce2e-41cf-afbf-52eaf128e825
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 26
    column: 2
    function: main
  location_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c6fe3b4-9d12-478e-aa0f-85873ba696aa
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 26
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22d7b1d6-38a3-48f7-9128-bcf64807b3b7
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 27
    column: 2
    function: main
  location_invariant:
    string: -10LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43d2f827-534d-4264-b98f-ca5f0f8c9329
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 27
    column: 2
    function: main
  location_invariant:
    string: 255LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 659342c9-2df6-4b2c-ba34-6bce4a18a838
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 27
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc24cd46-d0ef-4769-a1f7-ba5a1a91c292
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 27
    column: 2
    function: main
  location_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73a19439-f81f-4bd2-ada3-2ef9c47b05b2
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 27
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1891f80-a731-4424-ac10-f27805bd694c
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 28
    column: 2
    function: main
  location_invariant:
    string: 255LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7b6fc7d-4a2f-4763-9cfd-616655797f69
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 28
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e1a44ce-54c3-46de-81eb-494a504b9503
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 28
    column: 2
    function: main
  location_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5fe10f2a-0ce8-4dce-8b19-33d69af8f0dc
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 28
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a20e87d3-f3fb-491e-b790-4260e9e35940
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (unsigned char)48 <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db016632-3fa7-4ad4-8507-a559dfd4796f
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 31
    column: 4
    function: main
  location_invariant:
    string: c <= (unsigned char)57
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29898e83-c2c2-497f-a5d0-ed1c59f92fbd
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 31
    column: 4
    function: main
  location_invariant:
    string: -48LL + (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b51e2fed-094a-4df5-a0d9-f9a70ceefd7e
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 57LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3fc0eda-473a-48ff-8188-2eb73662f788
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )idx_in >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6528f7a4-b1ff-45a3-bf03-a31734c4a32d
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 31
    column: 4
    function: main
  location_invariant:
    string: c != (unsigned char)0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 527e1dd6-06a7-4f97-a797-2a1655be729b
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 32
    column: 4
    function: main
  location_invariant:
    string: j <= 9U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0aca0865-a997-4e64-a74f-99440d62c82b
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 32
    column: 4
    function: main
  location_invariant:
    string: -48LL + (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5326d797-d3bd-44f0-a6bf-24f6256784c2
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 57LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3fd75682-73f2-43cb-bef5-933c2a453110
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )idx_in >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4560b417-09f7-4fa5-9361-6dc22327b413
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 0 <= idx_in
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a797d134-1cf3-41a9-ad41-4210ed866a74
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 33
    column: 4
    function: main
  location_invariant:
    string: -48LL + (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 812fe181-bdc4-49ac-850e-4ce576ff84c4
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 57LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9244f91-8ccb-40d2-8479-857ca89267ca
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )idx_in >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b4a3a46-3021-477c-85ad-b79ecc12dea4
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 1 <= idx_in
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ebfd41d-1f91-4d81-b5fc-206b2cf620b3
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -48LL + (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f380f03-12b4-4fd3-af0c-9ab395316851
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 34
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )idx_in >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01920870-9e78-4ab8-b9b3-1db396008788
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 57LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b3eb6eb-d878-44f8-a10c-5efb1baebba2
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 37
    column: 2
    function: main
  location_invariant:
    string: (long long )idx_in >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cbea6f2e-f80c-4e74-864c-f0c49fec146b
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 38
    column: 2
    function: main
  location_invariant:
    string: (long long )idx_in >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ca1cb06-be2c-4d1a-a526-b59dd7fcd6dc
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 21
    column: 4
    function: main
  location_invariant:
    string: i <= 9U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2705c07e-c8cb-4ac9-b080-fe5520481c40
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 21
    column: 4
    function: main
  location_invariant:
    string: 9LL - (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c24a61db-5402-4cc2-bc53-f6f0f920210a
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 21
    column: 4
    function: main
  location_invariant:
    string: 255LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f380839e-4fcd-431e-8fad-c4a72a1d435b
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 21
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34ad96ec-ca81-40bb-b852-fe5cb5f06be6
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 21
    column: 4
    function: main
  location_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3aed4420-1b91-49ac-b3a5-c4f618038844
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 21
    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: 8f2a2daf-c05c-42a1-92ba-4d9752abcd8a
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 21
    column: 4
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60153a2b-1774-4d42-aad5-65791630c971
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 24
    column: 2
    function: main
  location_invariant:
    string: -10LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20d2e937-e9d9-467f-b508-2062eaf68482
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 24
    column: 2
    function: main
  location_invariant:
    string: 255LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 854895e4-59fc-4286-a55c-2b14c97259cd
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 24
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0546096d-a5a3-4e63-8717-727df2ea5d20
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 24
    column: 2
    function: main
  location_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0988ee42-ab71-4828-9f41-46497dc1c9f5
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 24
    column: 2
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a949b8f2-f2f8-4f80-9341-5be5da959792
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 29
    column: 10
    function: main
  loop_invariant:
    string: 0 <= idx_in
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a1d5ed25-6a3c-4107-9a6b-6a37cf869f20
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 29
    column: 10
    function: main
  loop_invariant:
    string: (long long )idx_in >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bdf26dbf-21b7-4650-8696-9e1f333da645
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 20
    column: 6
    function: main
  loop_invariant:
    string: i <= 10U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b02fff71-1317-4f8b-bbac-fadb111c82af
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 20
    column: 6
    function: main
  loop_invariant:
    string: 255LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 80ba6c41-619a-4b22-924b-685930750537
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 20
    column: 6
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f24a76c7-484b-42ea-aa65-bfc693f12508
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 20
    column: 6
    function: main
  loop_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 430b68ce-602c-4c49-9ac8-5ee2578ba94c
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 20
    column: 6
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b86476cd-bec7-458a-a672-5c7a5561d451
    creation_time: 2023-01-27T16:31:10Z
    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/veris.c_sendmail_tTflag_arr_one_loop.c'''
    task:
      input_files:
      - ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
      input_file_hashes:
        ../plain/veris.c_sendmail_tTflag_arr_one_loop.c: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/veris.c_sendmail_tTflag_arr_one_loop.c
    file_hash: d3ed36aa6701f38e4437e494734e2c4cd3d174950cdc9cef44311577dda2ee95
    line: 20
    column: 6
    function: main
  loop_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
