Add SMT Unknown Error

liquidjava-example/src/main/java/testSuite/CorrectPrimitiveNumbersTypes.java → liquidjava-example/src/main/java/testSuite/ErrorPrimitiveNumbersTypes.java

@@ -3,25 +3,25 @@
 import liquidjava.specification.Refinement;
 
 @SuppressWarnings("unused")
-public class CorrectPrimitiveNumbersTypes {
+public class ErrorPrimitiveNumbersTypes {
     @Refinement("_ < i && _ > 0")
     private static double fromType(@Refinement("_ > 0") int i) {
-        return i * 0.1;
+        return i * 0.1; // Expect: SMT Unknown Error
     }
 
     @Refinement(" _ < i && _ > 0")
     private static double fromType(@Refinement("_ > 0") long i) {
-        return i * 0.1;
+        return i * 0.1; // Expect: SMT Unknown Error
     }
 
     @Refinement(" _ < i && _ > 0")
     private static double fromType(@Refinement("_ > 0") short i) {
-        return i * 0.1;
+        return i * 0.1; // Expect: SMT Unknown Error
     }
 
     @Refinement("_ > i")
     private static float twice(@Refinement("i > 0") short i) {
-        return i * 2f;
+        return i * 2f; // Expect: SMT Unknown Error
     }
 
     public static void main(String[] args) {

liquidjava-example/src/main/java/testSuite/ErrorSMTUnknown.java

@@ -0,0 +1,10 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorSMTUnknown {
+    @Refinement("_ > 2.0")
+    public static int aboveTwo(int value) {
+        return value; // Expect: SMT Unknown Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorSMTUnknownState.java

@@ -0,0 +1,19 @@
+package testSuite;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("int amount")
+public class ErrorSMTUnknownState {
+    @StateRefinement(to = "amount(this) > 0")
+    public ErrorSMTUnknownState() {}
+
+    @StateRefinement(from = "amount(this) < limit")
+    public void consume(int limit) {}
+
+    public static void test(double limit) {
+        ErrorSMTUnknownState value = new ErrorSMTUnknownState();
+        int boundary = (int) limit;
+        value.consume(boundary); // Expect: SMT Unknown Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java

@@ -21,7 +21,7 @@
  * <ul>
  * <li>{@link #info} — verification context (caller-level predicates, source position).</li>
  * <li>{@link #smtStart} — premises and conclusion as fed to Z3.</li>
- * <li>{@link #smtUnsat} / {@link #smtSat} / {@link #smtUnknown} — solver outcome.</li>
+ * <li>{@link #smtUnsat} / {@link #smtSat} / {@link #smtError} — solver outcome.</li>
  * </ul>
  */
 public final class DebugLog {
@@ -400,16 +400,9 @@ private static String formatCounterexample(Object counterexample) {
         return sb.toString();
     }
 
-    public static void smtUnknown() {
-        if (!enabled()) {
-            return;
-        }
-        System.out.println(SMT_TAG + " Result: " + Colors.YELLOW + "UNKNOWN (treated as OK)" + Colors.RESET);
-    }
-
     /**
      * Print the result of an SMT check whose {@code smtStart} was emitted by the caller (e.g. VCChecker's structured
-     * print). {@link liquidjava.smt.SMTResult} doesn't preserve UNKNOWN, so this maps OK → UNSAT and ERROR → SAT.
+     * print). This maps OK → UNSAT and ERROR → SAT; UNKNOWN raises an error instead of returning a result.
      */
     public static void smtResult(liquidjava.smt.SMTResult result) {
         if (!enabled()) {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SMTUnknownError.java

@@ -0,0 +1,28 @@
+package liquidjava.diagnostics.errors;
+
+import spoon.reflect.cu.SourcePosition;
+
+/**
+ * Error indicating that the SMT solver could not decide a verification condition
+ */
+public class SMTUnknownError extends LJError {
+    private SourcePosition declarationPosition;
+
+    public SMTUnknownError(String reason) {
+        super("SMT Unknown Error", "Could not prove refinement", null, null);
+        String tacticFailure = "smt tactic failed to show goal to be sat/unsat ";
+        if (reason.startsWith(tacticFailure)) {
+            reason = reason.substring(tacticFailure.length()).replace("(", "").replace(")", "");
+        }
+        setHint("Reason: " + reason);
+    }
+
+    public void setDeclarationPosition(SourcePosition declarationPosition) {
+        this.declarationPosition = declarationPosition;
+    }
+
+    @Override
+    public SourcePosition getDeclarationPosition() {
+        return declarationPosition;
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -70,6 +70,10 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         SMTResult result;
         try {
             result = dischargeToSMT(expected, premises, annotationValuePos, true);
+        } catch (SMTUnknownError error) {
+            error.setDeclarationPosition(declarationPosition);
+            DebugLog.smtError(error.getMessage());
+            throw error;
         } catch (RuntimeException ex) {
             DebugLog.smtError(ex.getMessage());
             throw ex;
@@ -94,7 +98,13 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
      */
     public void processSubtyping(Predicate type, Predicate expectedType, List<GhostState> list, CtElement element,
             SourcePosition declarationPosition, Factory f) throws LJError {
-        SMTResult result = verifySMTSubtypeStates(type, expectedType, list, element.getPosition(), f);
+        SMTResult result;
+        try {
+            result = verifySMTSubtypeStates(type, expectedType, list, element.getPosition(), f);
+        } catch (SMTUnknownError error) {
+            error.setDeclarationPosition(declarationPosition);
+            throw error;
+        }
         if (result.isError())
             throwRefinementError(element.getPosition(), declarationPosition, expectedType, type,
                     result.getCounterexample(), null);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -7,6 +7,7 @@
 import liquidjava.diagnostics.errors.IllegalConstructorTransitionError;
 import liquidjava.diagnostics.errors.InvalidRefinementError;
 import liquidjava.diagnostics.errors.LJError;
+import liquidjava.diagnostics.errors.SMTUnknownError;
 import liquidjava.processor.context.*;
 import liquidjava.processor.refinement_checker.TypeChecker;
 import liquidjava.processor.refinement_checker.TypeCheckingUtils;
@@ -433,7 +434,14 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
         Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName)
                 .changeOldMentions(vi.getName(), instanceName);
 
-        if (!tc.checkStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition
+        boolean validTransition;
+        try {
+            validTransition = tc.checkStateSMT(prevState, expectState, fw.getPosition());
+        } catch (SMTUnknownError error) {
+            error.setDeclarationPosition(field.getDeclaringType().getPosition());
+            throw error;
+        }
+        if (!validTransition) { // Invalid field transition
             tc.throwStateRefinementError(fw.getPosition(), field.getDeclaringType().getPosition(), prevState,
                     expectState, stateChange.getMessage());
             return;
@@ -499,7 +507,12 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
             }
             expectState = expectState.changeOldMentions(vi.getName(), instanceName);
 
-            found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition());
+            try {
+                found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition());
+            } catch (SMTUnknownError error) {
+                error.setDeclarationPosition(stateChange.getFromPosition());
+                throw error;
+            }
             if (found && stateChange.hasTo()) {
                 String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
                 // Non-void: `_` is the return value; void: legacy alias for the new instance.

liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java

@@ -8,6 +8,7 @@
 import com.microsoft.z3.Z3Exception;
 
 import liquidjava.diagnostics.DebugLog;
+import liquidjava.diagnostics.errors.SMTUnknownError;
 import liquidjava.processor.context.Context;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
@@ -51,12 +52,15 @@ public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context conte
                     }
                     return SMTResult.error(counterexample);
                 }
-                if (!silent) {
-                    if (result.equals(Status.UNKNOWN)) {
-                        DebugLog.smtUnknown();
-                    } else {
-                        DebugLog.smtUnsat();
+                if (result.equals(Status.UNKNOWN)) {
+                    SMTUnknownError error = new SMTUnknownError(solver.getReasonUnknown());
+                    if (!silent) {
+                        DebugLog.smtError(error.getMessage());
                     }
+                    throw error;
+                }
+                if (!silent) {
+                    DebugLog.smtUnsat();
                 }
             }
         } catch (SyntaxException e) {