- entry_type: "loop_invariant"
  metadata:
    format_version: "0.1"
    uuid: "011b7e6a-9975-4609-abf6-0338fea52216"
    creation_time: "2023-01-31T11:35:12Z"
    producer:
      name: "CPAchecker"
      version: "2.2"
      configuration: "witness2invariant"
    task:
      input_files:
      - "/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i"
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i: "1fa7c9a8ed8874a508931184bf09b1ee30162cb6ccbf87de6b2ebe54845cfa76"
      specification: "G ! call(reach_error())"
      data_model: "LP64"
      language: "C"
  location:
    file_name: "/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i"
    file_hash: "file_hash"
    line: 16
    column: 2
    function: "main"
  loop_invariant:
    string: "x == (19) || x == (28) || x == (16) || x == (9) || x == (7) || x == (3) || x == (32) || x == (20) || x == (21) || x == (24) || x == (23) || x == (35) || x == (37) || x == (30) || x == (5) || x == (12) || x == (33) || x == (17) || x == (8) || x == (40) || (!(x == (40)) && x == (31)) || (!(x == (40)) && x == (26)) || (!(x == (40)) && x == (10)) || (!(x == (40)) && x == (25)) || (!(x == (40)) && x == (1)) || (!(x == (40)) && x == (27)) || (!(x == (40)) && x == (14)) || (!(x == (40)) && x == (34)) || (!(x == (40)) && x == (13)) || (!(x == (40)) && x == (22)) || (!(x == (40)) && x == (0)) || (!(x == (40)) && x == (6)) || (!(x == (40)) && x == (29)) || (!(x == (40)) && x == (18)) || (!(x == (40)) && x == (2)) || (!(x == (40)) && x == (39)) || (!(x == (40)) && x == (11)) || (!(x == (40)) && x == (38)) || (!(x == (40)) && x == (15)) || (!(x == (40)) && x == (4)) || (!(x == (40)) && x == (36))"
    type: "assertion"
    format: "C"
- entry_type: "loop_invariant"
  metadata:
    format_version: "0.1"
    uuid: "9c33b3f7-ab38-44c9-993d-d5a202aa3de6"
    creation_time: "2023-01-31T11:35:12Z"
    producer:
      name: "CPAchecker"
      version: "2.2"
      configuration: "witness2invariant"
    task:
      input_files:
      - "/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i"
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i: "1fa7c9a8ed8874a508931184bf09b1ee30162cb6ccbf87de6b2ebe54845cfa76"
      specification: "G ! call(reach_error())"
      data_model: "LP64"
      language: "C"
  location:
    file_name: "/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i"
    file_hash: "file_hash"
    line: 21
    column: 2
    function: "main"
  loop_invariant:
    string: "x == (0)"
    type: "assertion"
    format: "C"
- entry_type: "loop_invariant"
  metadata:
    format_version: "0.1"
    uuid: "fdc1711a-713c-4b85-86c9-4899ed0ed15d"
    creation_time: "2023-01-31T11:35:12Z"
    producer:
      name: "CPAchecker"
      version: "2.2"
      configuration: "witness2invariant"
    task:
      input_files:
      - "/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i"
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i: "1fa7c9a8ed8874a508931184bf09b1ee30162cb6ccbf87de6b2ebe54845cfa76"
      specification: "G ! call(reach_error())"
      data_model: "LP64"
      language: "C"
  location:
    file_name: "/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.6.i"
    file_hash: "file_hash"
    line: 17
    column: 4
    function: "main"
  loop_invariant:
    string: "x == (37) || x == (36) || x == (1) || x == (24) || x == (23) || x == (33) || x == (17) || x == (26) || x == (10) || x == (25) || x == (19) || x == (2) || x == (38) || x == (29) || x == (7) || x == (28) || x == (9) || x == (35) || x == (13) || x == (22) || x == (5) || x == (34) || x == (14) || x == (30) || x == (27) || x == (4) || x == (32) || x == (16) || x == (39) || x == (18) || x == (31) || x == (21) || x == (20) || x == (8) || x == (3) || x == (15) || x == (12) || x == (40) || (!(x == (40)) && x == (6)) || (!(x == (40)) && x == (11))"
    type: "assertion"
    format: "C"
