Add back test

tests/cargo-kani/mir-linker/Cargo.toml

@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "mir-linker"
+version = "0.1.0"
+edition = "2021"
+description = "Ensures that the mir-linker works accross crates"
+
+[dependencies]
+semver = "1.0"

tests/cargo-kani/mir-linker/expected

@@ -0,0 +1,3 @@
+Status: SUCCESS\
+Next is greater\
+in function check_version

tests/cargo-kani/mir-linker/src/lib.rs

@@ -0,0 +1,29 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Dummy test to check --mir-linker runs on a cargo project.
+use semver::{BuildMetadata, Prerelease, Version};
+
+#[kani::proof]
+fn check_version() {
+    let next_major: u64 = kani::any();
+    let next_minor: u64 = kani::any();
+    kani::assume(next_major != 0 || next_minor != 0);
+
+    // Check whether this requirement matches version 1.2.3-alpha.1 (no)
+    let v0 = Version {
+        major: 0,
+        minor: 0,
+        patch: 0,
+        pre: Prerelease::EMPTY,
+        build: BuildMetadata::EMPTY,
+    };
+    let next = Version {
+        major: next_major,
+        minor: next_minor,
+        patch: 0,
+        pre: Prerelease::EMPTY,
+        build: BuildMetadata::EMPTY,
+    };
+    assert!(next > v0, "Next is greater");
+}