- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3efc2b47-b0dd-478d-9a23-3eb29ede07c5
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 31
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1172bdaf-bcb1-4f93-8026-e1fbb024d2c9
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 31
    column: 8
    function: main
  location_invariant:
    string: x <= 2147483648LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26ffeb3a-4cf0-4655-aa35-4fd21b7cd691
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 31
    column: 8
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 250f0dc7-63a5-4441-a8be-b309098778ab
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 31
    column: 8
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9612b426-25c4-4b86-8cde-5ec7a5b177c7
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 32
    column: 8
    function: main
  location_invariant:
    string: -4611686018427387904LL <= yx
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec459e5a-e75f-475c-850e-07feeb1e5f42
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 32
    column: 8
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de391c21-2f78-423b-ab99-c205b1a6a83a
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 32
    column: 8
    function: main
  location_invariant:
    string: yx <= 4611686016279904256LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e8e960d-0b01-4822-97e1-376886128a6d
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 32
    column: 8
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6c922f4-42be-4ebe-8d10-14b88542de89
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 32
    column: 8
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 866f950b-4a72-4528-ba11-bc9d61687cdd
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 33
    column: 1
    function: main
  location_invariant:
    string: -4611686018427387904LL <= yx
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea9e5925-468c-4bff-9f29-642f10cca75b
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 33
    column: 1
    function: main
  location_invariant:
    string: yx <= 4611686016279904256LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4c3c238-f67b-4ada-810a-9e13ade50ab1
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 33
    column: 1
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bb43486-f6cd-4eb4-9355-59234ae7df7a
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 33
    column: 1
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d63902b7-da86-474d-8240-50e9fcb32a18
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 34
    column: 12
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b47c846b-2dc8-4649-a701-72ce199b2431
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 34
    column: 12
    function: main
  location_invariant:
    string: x <= 2147483648LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f9cfba9-9459-4d8b-b128-d1feb66d0a29
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 34
    column: 12
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79231a33-86b9-4383-a054-93df15837852
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 34
    column: 12
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 789534dc-f23a-4f66-a68f-3edebb44cbe7
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 38
    column: 12
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 983f666c-bf35-40af-86d7-052fdc6bbfb7
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 38
    column: 12
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e44e9c1-7cc0-406f-b4eb-9afec592c286
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 38
    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: c88725cd-c6f6-40a0-913e-84d762da47f7
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 39
    column: 12
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20d06c97-e287-4999-9cbe-bdb7389db812
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 39
    column: 12
    function: main
  location_invariant:
    string: v <= -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4ecc19e-1996-480d-9591-57970179e2c6
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 39
    column: 12
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7067809-8c02-4999-a248-9490d925b436
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 39
    column: 12
    function: main
  location_invariant:
    string: -1LL - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a21fe3c-1aed-4bb8-82ff-8597d4b951f4
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 39
    column: 12
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7034e3ee-71b1-4b1b-987e-3240053638f7
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 39
    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: 2323f77f-1c7f-4f60-a2ef-c791f5f1db8b
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 39
    column: 12
    function: main
  location_invariant:
    string: v != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b51a315a-5626-4c2a-9a37-1b6bd440198b
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 41
    column: 12
    function: main
  location_invariant:
    string: 0 <= X
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2da8ba8f-dffc-4813-8ea9-d4e94c9c6ae9
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 41
    column: 12
    function: main
  location_invariant:
    string: 0LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7406b963-c6ad-4db5-8f63-08cb24003091
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: 507bf473-9ebe-43b1-b005-88acc518615b
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: 1a7c2145-fbd9-4b96-8db0-35ebe00c82fc
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: 6cc712ae-057f-4916-9cdb-3c0b28654508
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: 93789b3f-34c7-4161-91e7-7db93894609b
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 42
    column: 12
    function: main
  location_invariant:
    string: -8589934590LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1292583a-34bd-4c17-8b28-919f82faa883
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 42
    column: 12
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f50a7395-20a6-4f1c-a0c6-334838c21f19
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 42
    column: 12
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5c56743-eda5-478a-ab1c-f10b0bbedcbc
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 42
    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: 957eac7a-98a0-4cb6-9eea-a11ca627b96c
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 42
    column: 12
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b177eb0-1d39-45d5-833c-9a8daf7d19b3
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 42
    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: 79b0322e-5898-4e53-b0dd-9b46341a3322
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 44
    column: 8
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5a14c7f-5806-4aec-8b97-c5dc4c91cb13
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 44
    column: 8
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5fe9b6f-a931-483e-b026-2ec38b4cb493
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 44
    column: 8
    function: main
  location_invariant:
    string: x <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b951dfd-c041-4fd3-849d-db82fdfda807
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 44
    column: 8
    function: main
  location_invariant:
    string: x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c84d14f-842b-4492-a873-ddbb12075dae
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 44
    column: 8
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ae5815a-4b45-4a19-8605-b791752e004b
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 44
    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: 2d459e9d-e4ef-4940-ba80-29ef5f96f6b7
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 44
    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: 2a2d7c5f-c2f2-4a8b-8a1e-3a2fd087e865
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 46
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6fd9e64d-ec41-440e-84c6-225731ec9248
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 46
    column: 4
    function: main
  location_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 441224b7-2dbe-41b6-9dab-e3d54303326a
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 46
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483648LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df1e89f6-a10a-4623-b7c1-c519235bd7c5
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 46
    column: 4
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c45ed283-3d1a-47a5-8a28-e16c39d1b697
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 46
    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: c0ec5d97-9da4-4186-857c-b508cdbaba73
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 46
    column: 4
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9b65d8d-d6ad-4885-9be8-2063aa86dc63
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 47
    column: 4
    function: main
  location_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09fbaa51-9a28-431e-a98a-1d99c3201139
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 47
    column: 4
    function: main
  location_invariant:
    string: 0LL <= xy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eeccdc99-964f-413d-aaa1-9b5cbeea33f2
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 47
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483648LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 784f6636-6ace-4610-9ca7-c1b936f4376e
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 47
    column: 4
    function: main
  location_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd0aeb45-43c2-4de0-81bd-4398887767f1
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 47
    column: 4
    function: main
  location_invariant:
    string: xy >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8c4b30a-af50-4225-8bbc-dec44c3de832
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 47
    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: 284dfc38-a39f-4c99-8c9c-d0e2190d00f3
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 47
    column: 4
    function: main
  location_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 367623c0-2869-4709-a146-0cf2cd20b92d
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 48
    column: 4
    function: main
  location_invariant:
    string: -4611686018427387904LL <= yx
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e25780eb-6ee7-45d1-a957-1544c4f63084
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: f85075f8-8c80-45d6-8192-af84e09264ce
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 48
    column: 4
    function: main
  location_invariant:
    string: 0LL <= xy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a5bca94-a88f-4fc9-83bf-77f98afe3efc
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 48
    column: 4
    function: main
  location_invariant:
    string: yx <= 4611686016279904256LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44a8f071-9b61-4392-ad97-718866659ab0
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: f32df378-e724-4042-952d-bd2b60f1ef52
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 48
    column: 4
    function: main
  location_invariant:
    string: xy >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1bf6eb7-0c73-44e8-b2c9-045904f729c0
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: 207d6b0f-c24e-4c09-b216-a98c8e096f32
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: 238f2253-9437-4ad8-864a-c46f1b27e5d1
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: 6193df0d-0a1b-43b4-ab64-6e990cb5eabd
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: 74498972-4b90-4210-8038-328cb17e9859
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: d92660b6-565c-4091-a12d-3129fbddd28d
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    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: d7aa84d2-2e56-467c-ad64-883f8efb9888
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 27
    column: 4
    function: main
  location_invariant:
    string: -6442450943LL <= v
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2711391a-0aec-40e5-8d54-fe8cf63bf05c
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 27
    column: 4
    function: main
  location_invariant:
    string: v <= 6442450942LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 898d2dbe-37b2-4c1b-8d54-afc0d5c28f17
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 337a16c9-2e41-4e91-a0a1-8c42cbd31ebd
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d9eb39ec-30ae-49ba-9878-4d4a98238704
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: x <= 2147483648LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7919668e-33d3-46a7-b220-61d6312859bb
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0f0b62e0-6cd3-4ae2-a844-ff17f391bec0
    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.c'''
    task:
      input_files:
      - ../plain/bresenham-ll.c
      input_file_hashes:
        ../plain/bresenham-ll.c: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/bresenham-ll.c
    file_hash: 68505a1040934ea3cdccf61a3fb1a3debf8c6c64330c175637d96b2737c92d5f
    line: 30
    column: 11
    function: main
  loop_invariant:
    string: x - y >= 0LL
    type: assertion
    format: C
