Rename Warning

Author: rcosta358

…ics/warnings/UnsatRefinementWarning.java …ings/UnsatisfiableRefinementWarning.javaliquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/UnsatRefinementWarning.java renamed to liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/UnsatisfiableRefinementWarning.java liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/UnsatRefinementWarning.java renamed to liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/UnsatisfiableRefinementWarning.java

@@ -7,12 +7,12 @@
  * 
  * @see LJWarning
  */
-public class UnsatRefinementWarning extends LJWarning {
+public class UnsatisfiableRefinementWarning extends LJWarning {
 
     private final String refinement;
 
-    public UnsatRefinementWarning(SourcePosition position, String message, String refinement) {
-        super(message, position);
+    public UnsatisfiableRefinementWarning(SourcePosition position, String refinement) {
+        super("This refinement can never be true", position);
         this.refinement = refinement;
     }
 

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

@@ -8,7 +8,7 @@
 
 import liquidjava.diagnostics.Diagnostics;
 import liquidjava.diagnostics.errors.*;
-import liquidjava.diagnostics.warnings.UnsatRefinementWarning;
+import liquidjava.diagnostics.warnings.UnsatisfiableRefinementWarning;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostFunction;
@@ -131,7 +131,7 @@ private void checkRefinementSatisfiability(String refinement, Predicate predicat
 
             if (new SMTEvaluator().isUnsatisfiable(refinementPredicate, context)) {
                 SourcePosition position = Utils.getLJAnnotationPosition(element, refinement);
-                diagnostics.add(new UnsatRefinementWarning(position, "This refinement can never be true", refinement));
+                diagnostics.add(new UnsatisfiableRefinementWarning(position, refinement));
             }
             element.putMetadata(Keys.REFINEMENT_SAT_CHECK, true); // for caching the satisfiability check result
         } catch (Exception e) {