# This file is part of the SV-Benchmarks collection of verification tasks:
# https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
#
# SPDX-FileCopyrightText: 2023-2025 Simmo Saan
#
# SPDX-License-Identifier: MIT

- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 0e84a9de-b9f6-44dd-ab8d-ebdeca941483
    creation_time: 2025-10-17T17:14:00Z
    producer:
      name: Simmo Saan
      version: n/a
    task:
      input_files:
      - mine2017-ex4.6.c
      input_file_hashes:
        mine2017-ex4.6.c: 543af0d5de8128e2a70ef5165e255b68288cac9b22ac9c5f5408c2a6cc1efe34
      specification: G ! call(reach_error())
      data_model: LP64
      language: C
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: mine2017-ex4.6.c
        line: 11
        column: 3
        function: main
      value: 0 <= x && x <= 40
      format: c_expression
