- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b1aa2ec-b69e-4566-a5ec-3af201fe9c40
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 567ff233-d5e0-406e-9cb5-572bd5901fa1
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: 1 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9766e4da-4169-44ee-b0b8-d8e0165dbc74
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: 1 <= z
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e0074437-d4d5-4c37-a05b-195b8ca0c3b9
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: d <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f6272111-e5c4-4c12-a854-42125b2538cf
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: d <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 99500223-7ec6-469d-9df9-8a8778ce65b1
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: k <= 1073741823
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a1877c86-9a95-4944-bc42-82b4c0da329d
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: z <= 2147483644
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c96b729-1c7a-4c9c-9a53-255341bd81c2
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 27cab985-5c7e-4169-92ac-08a617d2d598
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: -1LL + (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 14203388-824c-4be2-87f8-77e1db953b2a
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: 1LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d61878ad-3f02-4864-abb6-ca96317644a5
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: 2LL - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 98e9b787-07a1-4f97-bc6a-0188fb8815b9
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: 1073741823LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ab30e6c4-5c5d-4ce6-b54f-ed6f1713c461
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c703914c-d820-491f-bdd5-52996a82fdb5
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 30
    column: 9
    function: f
  loop_invariant:
    string: d != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 73ca2f50-9e8f-48ac-91b7-97c738a978d1
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: -1000000 <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cfc0dd23-05f8-438e-83d6-8ef3539d1cab
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: -1000000 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bf7a63fe-963e-4340-9539-8dea2e9915e3
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: -1000000 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 002dc122-844d-46e1-bc49-23372bdcc698
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 834f0fda-4c60-4455-b6b0-822791aaffd9
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: 1 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f62b6e64-600f-41ac-8b84-29d9ec246903
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: d <= 2
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 04d62af8-4c7c-4331-b097-07ab932dfd62
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: d <= 127
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 40ea7f80-00e0-4c94-8fbb-c21908054af9
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b2946357-8204-4487-8f01-40c03416ebe7
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: y <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b51350ca-891e-4f1e-acd4-3a516136f78c
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: k <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e9cc6d3-2730-47db-a121-b3e81a051c47
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: z <= 2147483644
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 76a42e3a-cafd-4c08-a218-a775bdd24fbe
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: -1LL + (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 46c41c36-db22-4d87-a723-0b25eba4c83e
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: 1000000LL + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b2dd6d37-81be-4bca-b239-6d91ea5b26eb
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: 1LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b26a3eb-18b1-4556-90cc-27ac2c1c93cd
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: 2LL - (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f37007d-60b0-4c18-b53a-a14865e5403b
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: 1000000LL - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e3b8fefa-fcd5-4a7c-92ac-599d0ed8611e
    creation_time: 2023-01-27T15:24:22Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops/trex01-2.i
    file_hash: fcd99b2df0924887988cb47edc94be4a868bdcbcd74e734872c50b1f1ade5738
    line: 36
    column: 9
    function: f
  loop_invariant:
    string: d != 0
    type: assertion
    format: C
