- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7909b762-4300-463e-8135-e84aaa133645
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 0 <= Y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d087c472-3ce9-4489-82c0-fd7e802cb9b7
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )Y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 342987c1-c873-4147-b383-3932bd01391c
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 29
    column: 4
    function: main
  location_invariant:
    string: -6442450943LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ca8d958-cadd-48f9-8518-f9fc6962a20f
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 29
    column: 4
    function: main
  location_invariant:
    string: v <= 6442450942LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c314b10b-694a-4ebf-9112-a57fcdd6f736
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 33
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 618d0a4d-3733-4f1d-823d-15aae345f2be
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 33
    column: 8
    function: main
  location_invariant:
    string: x <= 2147483648LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 50f6ab57-0975-4770-9c3b-7b5439a8bddf
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 33
    column: 8
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e12b5d3-7557-455b-a4c6-c860a6dd6f11
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 33
    column: 8
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a4c1e39-b1cf-4479-843c-4228b4744094
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 34
    column: 8
    function: main
  location_invariant:
    string: -4611686018427387904LL <= yx
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 132a6da7-b76a-495e-a84e-51102366a0ae
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8671155-cf50-4fd4-8ee4-6d80afa7fdc1
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 34
    column: 8
    function: main
  location_invariant:
    string: yx <= 4611686016279904256LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f4073ca-d00a-438b-a16c-1b5de728e428
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 34
    column: 8
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d14640b0-3295-41df-8ac9-72debba712f1
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 34
    column: 8
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb089edf-da28-4931-98f9-907e83ca94c2
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 35
    column: 1
    function: main
  location_invariant:
    string: -4611686018427387904LL <= yx
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5b9cdd6-16fc-4134-8aca-c864a6a4ddc3
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 35
    column: 1
    function: main
  location_invariant:
    string: yx <= 4611686016279904256LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15a9d62f-93b7-495e-bbca-0fcb1b28095a
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 35
    column: 1
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f3c8a0a-9f44-4571-a10c-6677c8b3736e
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 35
    column: 1
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4bb84dc3-49e8-4748-af0c-86e5a5c318c7
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 36
    column: 12
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e93a8092-bc97-48f9-86f8-5d4770504ecd
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 36
    column: 12
    function: main
  location_invariant:
    string: x <= 2147483648LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 903da136-ba6d-465a-bd17-6b60ad05dc17
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 36
    column: 12
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aaec6568-7138-4e20-ba65-4d4fed2e0d55
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 36
    column: 12
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a82b386f-7827-4802-8878-25ef79b7c9dd
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 40
    column: 12
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 889a95e2-0c95-43a5-860b-60c7f38e68f1
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 40
    column: 12
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33b563eb-eae2-449d-b213-5b08c82de996
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 40
    column: 12
    function: main
  location_invariant:
    string: (long long )X - x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03d0ddac-15a9-4ccf-a1b5-28767c28c832
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 41
    column: 12
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd86696e-549d-4867-b184-36d7bd0f2271
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 41
    column: 12
    function: main
  location_invariant:
    string: v <= -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ddc0c6dd-7f1d-40ab-993b-48ec80756247
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 41
    column: 12
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2491aec0-ca7c-4ad0-a984-8d6940d94fe8
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 41
    column: 12
    function: main
  location_invariant:
    string: -1LL - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 13961758-e47d-4c41-9319-1b9fb123d1ba
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 41
    column: 12
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 602cffc9-71fb-42e5-abe3-40e783ab5895
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 41
    column: 12
    function: main
  location_invariant:
    string: (long long )X - x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 74d4e728-8a4b-4cf0-9a2c-1443632e5394
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 41
    column: 12
    function: main
  location_invariant:
    string: v != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 791faf64-f8a1-40ab-82b9-eac67165e512
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 0 <= X
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc9c6448-39ee-43e3-b8f7-428bb5ffaf5e
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 0LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4e1e617-9e43-4b66-b0d6-dcab781cd731
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 43
    column: 12
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 859d3e0c-81fa-4cdc-aef7-d85fe1489e48
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 43
    column: 12
    function: main
  location_invariant:
    string: v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d28aac02-42a8-4ca8-b427-24556069b2b6
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 43
    column: 12
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c1c33de-2885-4ba7-9d0e-82bfea2374d4
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 43
    column: 12
    function: main
  location_invariant:
    string: (long long )X - x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b55df3e-9fcc-4c0b-a934-ea933a602eb9
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 44
    column: 12
    function: main
  location_invariant:
    string: -8589934590LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14a4e2a1-67e1-460c-9dbe-7b60381cd89d
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 44
    column: 12
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cef4562a-c664-465f-8eb7-5e0388008a33
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 44
    column: 12
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e5e5745-0f3a-43fc-a864-3bbd7b84ac76
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 44
    column: 12
    function: main
  location_invariant:
    string: (2LL * (long long )X - 2LL * (long long )Y) + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 031d5210-15f8-4eff-a66e-bcef8a52b0f4
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 44
    column: 12
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19d6a3a8-14d5-4d88-aee2-6f7680e7b8fd
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 44
    column: 12
    function: main
  location_invariant:
    string: (long long )X - x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e71bf6c-8ecd-4f3d-a597-0f9be9e93499
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 46
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1e9b9d1e-4226-4b1f-873e-bec636982d6a
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 46
    column: 8
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 653b19e0-7551-42f5-95bd-3dbe98a789d0
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 46
    column: 8
    function: main
  location_invariant:
    string: x <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4dbe9752-a0ff-41f7-9736-5e45c5a47832
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 46
    column: 8
    function: main
  location_invariant:
    string: x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de9245ce-45d7-4fb9-ac23-7ab959e05b5f
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 46
    column: 8
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6496141-7570-4dc7-9748-bf1e1dd0b339
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 46
    column: 8
    function: main
  location_invariant:
    string: (1LL + x) - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cba13af8-d8a0-436e-8d4c-49adcf2b6187
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 46
    column: 8
    function: main
  location_invariant:
    string: (long long )X - x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 088ef657-6102-4876-99f9-8437c6be5b6a
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 48
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89c8cbb9-4a53-41c8-9ada-8c9839c2770f
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 48
    column: 4
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92edbc64-d38f-403e-980f-bce8c1b0f9b9
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 48
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483648LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89081d9c-a71a-466d-ae28-471aa4617257
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 48
    column: 4
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9bd06c31-d82e-4470-a20c-805232a93eb6
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 48
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )X) + x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c9d43be6-e360-4e14-bb17-5f4783e1d339
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 48
    column: 4
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c3c2dd01-0448-4056-8d1f-402f922cd196
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 49
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8281bd3-68cb-4db5-8881-b11da031086c
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 49
    column: 4
    function: main
  location_invariant:
    string: 0LL <= xy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51a2ff63-3394-4b13-9df7-09df689c3521
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 49
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483648LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad0388e8-7d8d-4e68-8df0-d96f4517d2dd
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 49
    column: 4
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34f9727c-a90d-4e99-8124-781edcabc0b9
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 49
    column: 4
    function: main
  location_invariant:
    string: xy >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44446614-363e-4160-b7dd-e53ddd1d8bed
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 49
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )X) + x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67026c64-0d31-4fc6-aade-d4e658029aa1
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 49
    column: 4
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6084e634-fcaa-4005-8678-879743620a5a
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 50
    column: 4
    function: main
  location_invariant:
    string: -4611686018427387904LL <= yx
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a17458d8-491a-48dd-a95b-db279b6b47c0
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 50
    column: 4
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d3f1cad8-dbb6-4149-818a-0db622839efb
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 50
    column: 4
    function: main
  location_invariant:
    string: 0LL <= xy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: afb23b1d-ddd3-4685-b9c0-6cdaa759fb15
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 50
    column: 4
    function: main
  location_invariant:
    string: yx <= 4611686016279904256LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 957c4b4d-48ae-4064-ae55-7e9b6f120074
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 50
    column: 4
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3316802c-6b37-4615-a78f-e2c67e06ffc4
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 50
    column: 4
    function: main
  location_invariant:
    string: xy >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb43e6de-b77a-4c51-adf3-b4dfe023cb64
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 50
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )X) + x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c55de088-f2e5-4146-853a-f458a1f2f278
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 50
    column: 4
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77b94736-9bd8-4a71-a300-2f5366b982dc
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 52
    column: 4
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e23fedb3-e879-4e98-9eba-b9a69d8a6895
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 52
    column: 4
    function: main
  location_invariant:
    string: xy >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6618b800-8a7c-4620-bb27-834dae802511
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 52
    column: 4
    function: main
  location_invariant:
    string: (-1LL - (long long )X) + x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70f82d6f-122b-4c32-8ce3-beaed244ded8
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 52
    column: 4
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f3996af-8d00-4ca7-8613-568c8e2037a1
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 0 <= X
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0568b8d-3997-43d1-a27c-f3fb5c77f39c
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )X >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 932ba785-961b-4fcf-845b-454ea8884c7c
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 18593c27-889b-4b26-ac3e-f8232accb511
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8eab3e95-83ef-4306-8e19-5ff5a5894c73
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: x <= 2147483648LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f55df40-b0a8-4bb6-a905-e009c4e27237
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ab363f37-2c7c-46f3-a1c7-f4f7b4487007
    creation_time: 2023-01-27T16:29:19Z
    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/bresenham-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound10.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound10.c: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound10.c
    file_hash: 4018f196b5be3ea7c518259557cd649a90434a9cacf1ef4108caf962c0feb788
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
