Fix Merge

Author: rcosta358

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

@@ -52,8 +52,8 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         }
         boolean isSubtype = smtChecks(expected, premises, element.getPosition());
         if (!isSubtype)
-            throw new RefinementError(element.getPosition(), expectedType.getExpression(),
-                    premisesBeforeChange.simplify(), map);
+            throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(),
+                    map);
     }
 
     /**
@@ -263,7 +263,7 @@ protected void throwRefinementError(SourcePosition position, Predicate expected,
         gatherVariables(found, lrv, mainVars);
         TranslationTable map = new TranslationTable();
         Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions();
-        throw new RefinementError(position, expected.getExpression(), premises.simplify(), map);
+        throw new RefinementError(position, expected.simplify(), premises.simplify(), map);
     }
 
     protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected)

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java

@@ -271,7 +271,7 @@ public void validateGhostInvocations(Context ctx, Factory f) throws LJError {
         if (this instanceof FunctionInvocation fi) {
             // get all ghosts with the matching name
             List<GhostFunction> candidates = ctx.getGhosts().stream().filter(g -> g.matches(fi.name)).toList();
-            if (candidates.isEmpty()) 
+            if (candidates.isEmpty())
                 return; // not found error is thrown elsewhere
 
             // find matching overload