From fc7458cdbaf833b4ff6d29e2cce4b6fb36b89457 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 19 Nov 2025 15:53:37 +0000
Subject: [PATCH 1/2] Remove misplaced Verifier file

This is part of the sv-benchmarks repository,
not sure why this is here.
---
 .../org/sosy_lab/sv_benchmarks/Verifier.java  | 72 -------------------
 1 file changed, 72 deletions(-)
 delete mode 100644 src/main/java/org/sosy_lab/sv_benchmarks/Verifier.java

diff --git a/src/main/java/org/sosy_lab/sv_benchmarks/Verifier.java b/src/main/java/org/sosy_lab/sv_benchmarks/Verifier.java
deleted file mode 100644
index 29d0e32..0000000
--- a/src/main/java/org/sosy_lab/sv_benchmarks/Verifier.java
+++ /dev/null
@@ -1,72 +0,0 @@
-/*
- * Contributed by Peter Schrammel
- *
- * Licensed under the Apache License, Version 2.0 (the "License");
- * you may not use this file except in compliance with the License.
- * You may obtain a copy of the License at
- *
- *         http://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing, software
- * distributed under the License is distributed on an "AS IS" BASIS,
- * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
- * See the License for the specific language governing permissions and
- * limitations under the License.
- */
-
-package org.sosy_lab.sv_benchmarks;
-
-import org.cprover.CProver;
-
-public final class Verifier
-{
-  public static void assume(boolean condition)
-  {
-    CProver.assume(condition);
-  }
-
-  public static boolean nondetBoolean()
-  {
-    return CProver.nondetBoolean();
-  }
-
-  public static byte nondetByte()
-  {
-    return CProver.nondetByte();
-  }
-
-  public static char nondetChar()
-  {
-    return CProver.nondetChar();
-  }
-
-  public static short nondetShort()
-  {
-    return CProver.nondetShort();
-  }
-
-  public static int nondetInt()
-  {
-    return CProver.nondetInt();
-  }
-
-  public static long nondetLong()
-  {
-    return CProver.nondetLong();
-  }
-
-  public static float nondetFloat()
-  {
-    return CProver.nondetFloat();
-  }
-
-  public static double nondetDouble()
-  {
-    return CProver.nondetDouble();
-  }
-
-  public static String nondetString()
-  {
-    return CProver.nondetWithoutNull("");
-  }
-}

From 5ce1ea45be2498902ddb78da3e6cc23997c9b2f8 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 19 Nov 2025 16:06:09 +0000
Subject: [PATCH 2/2] Enhance README wrt Usage and License

---
 README.md | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/README.md b/README.md
index 0df76f8..ca00fcf 100644
--- a/README.md
+++ b/README.md
@@ -5,3 +5,15 @@ This repository contains a version of the Java Class Library (`rt.jar`) that can
 be used together with
 [JBMC](https://github.com/diffblue/cbmc/tree/develop/jbmc) to
 model-check Java code that calls the standard library.
+
+## Usage
+
+Put the `core-models.jar` on the classpath of the application that you
+model-check using JBMC, e.g.
+```
+jbmc -cp .:cprover-api.jar:core-models.jar com.examples.MyClass.foo
+```
+
+## License
+
+[OpenJDK GPLv2 + Classpath Exception](https://github.com/openjdk/jdk/blob/master/LICENSE)