Fix AuxStateHandler

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java

@@ -181,7 +181,7 @@ public static void printCostumeError(CtElement element, String msg, ErrorEmitter
         sb.append(element + "\n\n");
         sb.append("Location: " + element.getPosition() + "\n");
         sb.append("______________________________________________________\n");
-        
+
         errorl.addError(s, sb.toString(), element.getPosition(), 1);
     }
 

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

@@ -119,7 +119,8 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
                 CtLiteral<String> s = (CtLiteral<String>) ce;
                 String f = s.getValue();
                 if (Character.isUpperCase(f.charAt(0))) {
-                    ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'", errorEmitter);
+                    ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'",
+                            errorEmitter);
                 }
             }
         }

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

@@ -81,13 +81,9 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
                 Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), s),
                         Predicate.createLit("0", Utils.INT));
                 c = Predicate.createConjunction(c, p);
-            } else if (sg.getReturnType().toString().equals("boolean")) {
-                Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
-                        Predicate.createLit("false", Utils.BOOLEAN));
-                c = Predicate.createConjunction(c, p);
             } else {
                 // TODO: Implement other stuff
-                throw new RuntimeException("Ghost Functions not implemented for other types than int/boolean -> implement in"
+                throw new RuntimeException("Ghost Functions not implemented for other types than int -> implement in"
                         + " AuxStateHandler defaultState");
             }
         }
@@ -635,4 +631,4 @@ private static List<CtAnnotation<? extends Annotation>> getStateAnnotation(CtEle
         // }
         // return l;
     }
-}
+}