- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a0711ef-4a5f-4407-8b04-940a319cfe05
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d33f681-30f0-4559-92ce-d192bfd219d5
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a07541c-c751-4889-971c-7861452b8a9d
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92a6df56-108c-449d-8375-3c51861dd176
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b5effd2-abf8-46ef-84bd-5439f9100512
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6d7a953-b58b-4fcc-95c6-73e8842a06bc
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1330c5ea-569b-4627-ab26-d752a69d4fa5
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e4fe31f2-e982-4cc4-8f83-99a066c1a93f
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a91ba59-a937-470b-b4f1-58badae16f29
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2271cdb8-e0c1-400b-83e1-d58b55216a6d
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c163f0e-da57-46d3-b8bc-c868996c3f13
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b193c8b-2209-4b55-bbb9-1fdaf70fd48a
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 88ef46ae-60b5-403a-b925-6db7e5a95b7b
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: baac5fe4-c583-4174-8306-fb33c9c42004
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ee609ee-a146-4df5-ba1e-745277767c51
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a87bef3-1cc6-4da5-959e-1631dae6a767
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2745b570-cbca-4ed4-8ba0-cbc941f38055
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d43c864-70d7-41bd-b648-e09a5fbd399d
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4892d6c-d9c9-4871-a0e4-4eea8b2e7625
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e10cb6fc-5597-49f5-b5b6-dc15e1dc97f2
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4175cbee-c6cb-4df8-8182-1c8d7495cde4
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b76721af-6116-4ec2-86d9-8e1138836ded
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 9
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((2147483647LL + (long long )iCheck) + (long
      long )iSet >= 0LL && (2147583648LL - (long long )iCheck) + (long long )iSet
      >= 0LL) && (100000LL + (long long )a) - (long long )iSet >= 0LL) && (100000LL
      + (long long )a) - (long long )iCheck >= 0LL) && (100001LL + (long long )b)
      - (long long )iSet >= 0LL) && (100001LL + (long long )b) - (long long )iCheck
      >= 0LL) && (2147583648LL + (long long )iCheck) - (long long )iSet >= 0LL) &&
      (100000LL - (long long )b) - (long long )iSet >= 0LL) && (100000LL - (long long
      )b) - (long long )iCheck >= 0LL) && (100001LL - (long long )a) - (long long
      )iSet >= 0LL) && (100001LL - (long long )a) - (long long )iCheck >= 0LL) &&
      (200000LL - (long long )iCheck) - (long long )iSet >= 0LL)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 258188b5-67be-44b8-9984-eaa998db8dcc
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 06450403-a47d-418a-8b95-446c2e8af6da
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1261
    column: 13
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 960bded1-aefc-45e4-9474-0b372e538732
    creation_time: 2024-06-18T15:14:03Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.activated[+]'' ''apron''
        ''--set'' ''ana.autotune.activated[-]'' ''octagon'' ''--enable'' ''ana.apron.invariant.diff-box''
        ''--disable'' ''ana.base.invariant.enabled'' ''--set'' ''ana.apron.domain''
        ''octagon'' ''--set'' ''ana.autotune.activated[-]'' ''wideningThresholds''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/reorder_5.i
    file_hash: 0517a9ebb69eeca4ecbb6ac063832eb703719698fb2ee670ca348e2c511f9dfd
    line: 1255
    column: 13
    function: main
