making sure that cuts work with boolean terms instead of formulas.

Author: mattulbrich

key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.java

@@ -51,8 +51,9 @@ static void execute(EngineState state, Parameters args) throws ScriptException {
         TacletApp app = NoPosTacletApp.createNoPosTacletApp(cut);
         SchemaVariable sv = app.uninstantiatedVars().iterator().next();
 
-        app = app.addCheckedInstantiation(sv, args.formula,
-            state.getProof().getServices(), true);
+        var formula = state.getProof().getServices().getTermBuilder().convertToFormula(args.formula);
+
+        app = app.addCheckedInstantiation(sv, formula, state.getProof().getServices(), true);
         state.getFirstOpenAutomaticGoal().apply(app);
     }
 

key.core/src/test/resources/de/uka/ilkd/key/scripts/jml/AssertedModelMethod.java

@@ -0,0 +1,23 @@
+//! settings:
+//!   CLASS_AXIOM_OPTIONS_KEY: CLASS_AXIOM_OFF
+
+// Was a bug:
+// Instantiation Test::pred(heap,self,int::select(heap,self,Test::$f)) of cutFormula (formula) does not satisfy the variable conditions
+
+class Test {
+
+    //@ model boolean pred(int x) { return x > 20; }
+
+    int f;
+
+    //@ requires pred(f);
+    //@ ensures f > 2;
+    void test() {
+        int x;
+        /*@ assert f > 2 \by {
+              assert pred(f) \by { auto classAxioms:true; }
+              auto; // should not be necessary ... eventually removed
+        } */
+    }
+
+}