Add SMT Unknown Error

Author: rcosta358

…tSuite/CorrectPrimitiveNumbersTypes.java …estSuite/ErrorPrimitiveNumbersTypes.javaliquidjava-example/src/main/java/testSuite/CorrectPrimitiveNumbersTypes.java renamed to liquidjava-example/src/main/java/testSuite/ErrorPrimitiveNumbersTypes.java liquidjava-example/src/main/java/testSuite/CorrectPrimitiveNumbersTypes.java renamed to 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-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,12 @@
+package liquidjava.diagnostics.errors;
+
+/**
+ * Error indicating that the SMT solver could not decide a verification condition
+ */
+public class SMTUnknownError extends LJError {
+
+    public SMTUnknownError(String reason) {
+        super("SMT Unknown Error",
+                "The SMT solver returned UNKNOWN and could not verify the refinement. Reason: " + reason, null, null);
+    }
+}

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) {