Add Expected Error to Test

Author: rcosta358

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

@@ -1,4 +1,4 @@
-
+// Refinement Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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

@@ -42,8 +42,8 @@ public static void storeVariablesSubtypes(Context z3, List<RefinedVariable> vari
     private static Expr<?> getExpr(Context z3, String name, CtTypeReference<?> type) {
         String typeName = type.getQualifiedName();
         return switch (typeName) {
-        case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" ->
-            z3.mkIntConst(name);
+        case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3
+                .mkIntConst(name);
         case "boolean", "java.lang.Boolean" -> z3.mkBoolConst(name);
         case "long", "java.lang.Long" -> z3.mkRealConst(name);
         case "float", "double", "java.lang.Float", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64());
@@ -82,8 +82,7 @@ private static void addBuiltinFunctions(Context z3, Map<String, FuncDecl<?>> fun
 
     static Sort getSort(Context z3, String sort) {
         return switch (sort) {
-        case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" ->
-            z3.getIntSort();
+        case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3.getIntSort();
         case "boolean", "java.lang.Boolean" -> z3.getBoolSort();
         case "long", "java.lang.Long" -> z3.getRealSort();
         case "float", "java.lang.Float" -> z3.mkFPSort32();