- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 471a8be4-cec8-4625-bcc8-c0cac269a963
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 5202392b-04fa-47f1-9847-15bbb62e906e
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 116a1a61-cf37-4f32-a753-b41662a378ec
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 604b3cc9-3b3e-4ef9-b0d8-b7f92591a01f
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 877537e1-0df7-41a0-b959-d33e21632fc9
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 0b053323-1b42-49f3-858e-bd001f247b00
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: e28e202a-183f-437a-904c-8c6963da315f
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: c9708115-620e-4ffe-97ee-4d9b5a328557
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 30a54ce5-5340-4a86-9d9d-babc31442ef1
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: a70c06b9-3a8f-4943-8b23-7db342e75eb8
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: ad21ab61-7827-4820-b3fe-6cdef68d1f57
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 8ee34af2-d3fb-4c5e-a6e3-02b55127a382
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: cf02340a-931a-4927-8b60-542603bbfdd1
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 3bc92c3f-40b9-4036-a6b5-c20651f11647
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 02a3a606-e18a-4cc6-8a2c-f866c34b6851
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: cc664ca0-1afd-4875-8394-627344e0dc0b
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 66bdcfe4-3ced-4f52-9d07-e5371d9146f7
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 09e681c1-fb89-4064-9d20-88bf46ddecb0
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 7cf39cd9-6442-43ff-b081-68b5ba86b55a
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 3c779a23-1d6d-4dc7-aedd-73efe6063342
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: d253abbf-dd35-494c-a804-08706fdfa77b
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 1e731239-df73-42d9-9c18-6a4b8bf0839b
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 6ceff15a-91cb-4131-8520-f010590cd89f
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 1bfabc0f-799c-48e3-bb5b-de9d2343af18
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 267a66b3-3356-46fe-9a19-050ed359c301
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: bafdcb44-5825-45e6-a849-6535a1bf6838
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 04a95286-6ea8-4133-9c72-98b348e8337b
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 0b39b809-b0ff-4895-b0e6-580036fba882
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: a181c345-eb7b-4dc4-afb1-53d566cd0e0a
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 469349db-5eff-4ef6-b9fa-049216655c7e
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: cf8fc553-97d3-4483-a411-caf5000c4c15
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 8955d76d-db01-4e9c-bd5c-2d54b944d51c
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 7aab8034-88c6-475d-ae87-1275fd8833e4
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: a56a785d-ca83-453c-bed0-ef9f3f65cad5
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: b67c36ac-fa5f-4f43-a947-5a57d5967b7f
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 4384acee-c69f-41ce-b978-0402ce5e6218
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 047c341d-e8ea-4f45-ade1-38adb2895639
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 5abeb217-c47f-41aa-9a4d-9a57a5158134
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: d755608f-5b80-45c1-986e-1f7bbd0d2280
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: ed65edf8-55f4-4730-947c-d70737bda149
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 0d69f18a-db35-4696-b8f5-64cd5dbf9c53
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 450fbe94-1b80-457f-a6d8-69be791045e3
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: f06d6876-5736-459f-9d44-188c9a7d80cf
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: c2e4fa81-4679-4c61-8f4b-92174b239689
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 399f4326-20e4-46b2-a42b-704eae845693
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: cffc38a0-604d-4e4f-919d-4e81516e83b6
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: e4cd57fb-2f91-405c-8f54-3ab2c3c33b76
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: abcf3357-f7a8-4ae7-b2fc-b83b8bf317b3
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 85a171f7-31e8-491d-afa5-d0efe92d1ccf
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 4725925f-407b-404e-b4b5-98ce08a053cb
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 80ef2c24-f537-4660-9b9c-bbcb622d0cf8
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 70fca650-d86e-492a-8656-b20ffb0d04a5
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: cbc5737a-e9d7-4467-9608-fb18ce4afda6
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 1fe4b827-276a-4be8-973b-c16c9736d35a
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: de978514-e8ea-4d5d-997d-7a2ff0f37473
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 526e8c6c-4576-49ff-946b-eb9e631d1f9c
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 29c85e27-507a-436b-9792-86f1ed295019
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 07c68753-2c38-4fab-982c-a9d219763171
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: a474a115-bd1c-4278-b7e6-90a693ee1e81
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 8a48f412-16a1-4531-9bcc-3ae225ef7366
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 2180b725-d800-4e68-a29d-8330861a7fbb
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 0e639a79-63c4-4bd9-b5e1-31dace18b05b
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 8e98fc7d-a0cd-4350-8aa6-2c848d940593
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 28df567f-af5f-40bf-8634-33bcfaf3c6c0
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 435517d6-9b0b-42f8-b9f8-dde77dc774ee
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: e6185b8c-30df-4163-bf93-1b63bc2e5e99
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: cbd40b81-c52d-471a-b244-ecef00a14a22
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: b3837834-b314-4ad9-b3f5-4ac8cf5b20e8
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: ca21d5d2-c434-4924-9ccd-761cc0a2c2fe
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: c407392c-9c73-47e2-b795-f075c821c07b
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 6109ed43-6bb8-4012-bd68-46db1ecd54e4
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 9b6ecb10-f15b-4105-b4ce-629d1936e177
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 6bfcf63f-38d0-4e44-9ca7-5fdb1205965c
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: d4ba6c2f-2446-4089-9459-415e83dfd362
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 42c75249-d134-4a8e-bff9-67cdc76add80
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 20540a8b-a344-4610-b195-51db13b8efb6
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: b79424e5-39cc-44bf-9ffe-d37a24752fb8
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 16b9522d-34f9-4013-b435-48eace03f73b
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 8efbc09c-af0b-45ff-a22d-1b1577bb0cfb
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 747ec3a2-7fa1-4359-9cf1-bca819e43182
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: a16a2c79-63c6-4042-a267-25f4c1899d43
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    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: 558a8873-bfc2-4e97-b30b-8bd5b31e24f8
    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_valuebound50.c'''
    task:
      input_files:
      - ../plain/bresenham-ll_valuebound50.c
      input_file_hashes:
        ../plain/bresenham-ll_valuebound50.c: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll_valuebound50.c
    file_hash: d998c441c771938676edf06a0e9387fce091f1e4d7230def291c87707c204f78
    line: 32
    column: 11
    function: main
  loop_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
