diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml
index 07abf74f..caaa0692 100644
--- a/liquidjava-verifier/pom.xml
+++ b/liquidjava-verifier/pom.xml
@@ -11,7 +11,7 @@
 
 	<groupId>io.github.liquid-java</groupId>
 	<artifactId>liquidjava-verifier</artifactId>
-	<version>0.0.14</version>
+	<version>0.0.15</version>
 	<name>liquidjava-verifier</name>
 	<description>LiquidJava Verifier</description>
 	<url>https://github.com/liquid-java/liquidjava</url>
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java
deleted file mode 100644
index 3383f6bf..00000000
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java
+++ /dev/null
@@ -1,12 +0,0 @@
-package liquidjava.diagnostics;
-
-import spoon.reflect.cu.SourcePosition;
-
-public record ErrorPosition(int lineStart, int colStart, int lineEnd, int colEnd) {
-
-    public static ErrorPosition fromSpoonPosition(SourcePosition pos) {
-        if (pos == null || !pos.isValidPosition())
-            return null;
-        return new ErrorPosition(pos.getLine(), pos.getColumn(), pos.getEndLine(), pos.getEndColumn());
-    }
-}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
index d1a743dc..affc6ae9 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
@@ -13,14 +13,14 @@ public class LJDiagnostic extends RuntimeException {
     private final String accentColor;
     private final String customMessage;
     private String file;
-    private ErrorPosition position;
+    private SourcePosition position;
     private static final String PIPE = " | ";
 
     public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) {
         this.title = title;
         this.message = message;
         this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null;
-        this.position = ErrorPosition.fromSpoonPosition(pos);
+        this.position = pos;
         this.accentColor = accentColor;
         this.customMessage = customMessage;
     }
@@ -41,14 +41,14 @@ public String getDetails() {
         return ""; // to be overridden by subclasses
     }
 
-    public ErrorPosition getPosition() {
+    public SourcePosition getPosition() {
         return position;
     }
 
     public void setPosition(SourcePosition pos) {
         if (pos == null)
             return;
-        this.position = ErrorPosition.fromSpoonPosition(pos);
+        this.position = pos;
         this.file = pos.getFile().getPath();
     }
 
@@ -82,7 +82,7 @@ public String toString() {
 
         // location
         if (file != null && position != null) {
-            sb.append("\n").append(file).append(":").append(position.lineStart()).append(Colors.RESET).append("\n");
+            sb.append("\n").append(file).append(":").append(position.getLine()).append(Colors.RESET).append("\n");
         }
 
         return sb.toString();
@@ -100,8 +100,8 @@ public String getSnippet() {
             // before and after lines for context
             int contextBefore = 2;
             int contextAfter = 2;
-            int startLine = Math.max(1, position.lineStart() - contextBefore);
-            int endLine = Math.min(lines.size(), position.lineEnd() + contextAfter);
+            int startLine = Math.max(1, position.getLine() - contextBefore);
+            int endLine = Math.min(lines.size(), position.getEndLine() + contextAfter);
 
             // calculate padding for line numbers
             int padding = String.valueOf(endLine).length();
@@ -115,9 +115,9 @@ public String getSnippet() {
                 sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n");
 
                 // add error markers on the line(s) with the error
-                if (i >= position.lineStart() && i <= position.lineEnd()) {
-                    int colStart = (i == position.lineStart()) ? position.colStart() : 1;
-                    int colEnd = (i == position.lineEnd()) ? position.colEnd() : rawLine.length();
+                if (i >= position.getLine() && i <= position.getEndLine()) {
+                    int colStart = (i == position.getLine()) ? position.getColumn() : 1;
+                    int colEnd = (i == position.getEndLine()) ? position.getEndColumn() : rawLine.length();
 
                     if (colStart > 0 && colEnd > 0) {
                         int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars()
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
index 23176dfd..c6e6fd46 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
@@ -104,32 +104,31 @@ public void addVarToContext(RefinedVariable var) {
         var.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
     }
 
-    public RefinedVariable addVarToContext(String simpleName, CtTypeReference<?> type, Predicate c,
-            CtElement placementInCode) {
+    public RefinedVariable addVarToContext(String simpleName, CtTypeReference<?> type, Predicate c, CtElement element) {
         RefinedVariable vi = new Variable(simpleName, type, c);
-        vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode));
+        vi.addPlacementInCode(element);
         vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
         addVarToContext(vi);
         return vi;
     }
 
     public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference<?> type, Predicate c,
-            CtElement placementInCode) {
+            CtElement element) {
         RefinedVariable vi = new VariableInstance(simpleName, type, c);
-        vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode));
+        vi.addPlacementInCode(element);
         if (!ctxInstanceVars.contains(vi))
             addInstanceVariable(vi);
         return vi;
     }
 
     public void addRefinementToVariableInContext(String name, CtTypeReference<?> type, Predicate et,
-            CtElement placementInCode) {
+            CtElement element) {
         if (hasVariable(name)) {
             RefinedVariable vi = getVariableByName(name);
             vi.setRefinement(et);
-            vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode));
+            vi.addPlacementInCode(element);
         } else {
-            addVarToContext(name, type, et, placementInCode);
+            addVarToContext(name, type, et, element);
         }
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java
index 0e4db162..cdd02ddf 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java
@@ -5,22 +5,23 @@
 import java.util.Map;
 import java.util.Set;
 
+import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
-import spoon.reflect.declaration.CtExecutable;
+import spoon.reflect.declaration.CtParameter;
 
 public class ContextHistory {
     private static ContextHistory instance;
 
-    private Map<String, Map<String, Set<RefinedVariable>>> fileScopeVars; // file -> (scope -> variables in scope)
-    private Set<RefinedVariable> instanceVars;
-    private Set<RefinedVariable> globalVars;
+    private Map<String, Set<String>> fileScopes;
+    private Set<RefinedVariable> localVars;
     private Set<GhostState> ghosts;
     private Set<AliasWrapper> aliases;
+    private Set<RefinedVariable> globalVars;
 
     private ContextHistory() {
-        fileScopeVars = new HashMap<>();
-        instanceVars = new HashSet<>();
+        fileScopes = new HashMap<>();
+        localVars = new HashSet<>();
         globalVars = new HashSet<>();
         ghosts = new HashSet<>();
         aliases = new HashSet<>();
@@ -33,48 +34,41 @@ public static ContextHistory getInstance() {
     }
 
     public void clearHistory() {
-        fileScopeVars.clear();
-        instanceVars.clear();
+        fileScopes.clear();
+        localVars.clear();
         globalVars.clear();
         ghosts.clear();
         aliases.clear();
     }
 
     public void saveContext(CtElement element, Context context) {
-        SourcePosition pos = element.getPosition();
-        if (pos == null || pos.getFile() == null)
+        String file = Utils.getFile(element);
+        if (file == null)
             return;
 
-        // add variables in scope for this position
-        String file = pos.getFile().getAbsolutePath();
+        // add scope
         String scope = getScopePosition(element);
-        fileScopeVars.putIfAbsent(file, new HashMap<>());
-        fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars()));
+        fileScopes.putIfAbsent(file, new HashSet<>());
+        fileScopes.get(file).add(scope);
 
-        // add other elements in context
-        instanceVars.addAll(context.getCtxInstanceVars());
+        // add variables, ghosts and aliases
+        localVars.addAll(context.getCtxVars());
+        localVars.addAll(context.getCtxInstanceVars());
         globalVars.addAll(context.getCtxGlobalVars());
         ghosts.addAll(context.getGhostStates());
         aliases.addAll(context.getAliases());
     }
 
-    public String getScopePosition(CtElement element) {
+    private String getScopePosition(CtElement element) {
+        CtElement startElement = element instanceof CtParameter<?> ? element.getParent() : element;
+        SourcePosition annPosition = Utils.getFirstLJAnnotationPosition(startElement);
         SourcePosition pos = element.getPosition();
-        SourcePosition innerPosition = pos;
-        if (element instanceof CtExecutable<?> executable) {
-            if (executable.getBody() != null)
-                innerPosition = executable.getBody().getPosition();
-        }
-        return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(),
+        return String.format("%d:%d-%d:%d", annPosition.getLine(), annPosition.getColumn(), pos.getEndLine(),
                 pos.getEndColumn());
     }
 
-    public Map<String, Map<String, Set<RefinedVariable>>> getFileScopeVars() {
-        return fileScopeVars;
-    }
-
-    public Set<RefinedVariable> getInstanceVars() {
-        return instanceVars;
+    public Set<RefinedVariable> getLocalVars() {
+        return localVars;
     }
 
     public Set<RefinedVariable> getGlobalVars() {
@@ -88,4 +82,8 @@ public Set<GhostState> getGhosts() {
     public Set<AliasWrapper> getAliases() {
         return aliases;
     }
+
+    public Map<String, Set<String>> getFileScopes() {
+        return fileScopes;
+    }
 }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java
index 121f0339..bbc51f73 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java
@@ -8,9 +8,12 @@ public class GhostState extends GhostFunction {
 
     private GhostFunction parent;
     private Predicate refinement;
+    private final String file;
 
-    public GhostState(String name, List<CtTypeReference<?>> list, CtTypeReference<?> returnType, String prefix) {
+    public GhostState(String name, List<CtTypeReference<?>> list, CtTypeReference<?> returnType, String prefix,
+            String file) {
         super(name, list, returnType, prefix);
+        this.file = file;
     }
 
     public void setGhostParent(GhostFunction parent) {
@@ -28,4 +31,8 @@ public GhostFunction getParent() {
     public Predicate getRefinement() {
         return refinement;
     }
+
+    public String getFile() {
+        return file;
+    }
 }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java
index 534f8cfa..7a04abde 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java
@@ -4,15 +4,21 @@
 import java.util.List;
 import java.util.Set;
 import liquidjava.rj_language.Predicate;
+import liquidjava.utils.Utils;
+import spoon.reflect.cu.SourcePosition;
+import spoon.reflect.declaration.CtElement;
 import spoon.reflect.reference.CtTypeReference;
 
 public abstract class RefinedVariable extends Refined {
     private final List<CtTypeReference<?>> supertypes;
     private PlacementInCode placementInCode;
+    private boolean isParameter;
+    private SourcePosition annPosition;
 
     public RefinedVariable(String name, CtTypeReference<?> type, Predicate c) {
         super(name, type, c);
         supertypes = new ArrayList<>();
+        isParameter = false;
     }
 
     public abstract Predicate getMainRefinement();
@@ -34,14 +40,23 @@ public void addSuperTypes(CtTypeReference<?> ts, Set<CtTypeReference<?>> sts) {
                 supertypes.add(ct);
     }
 
-    public void addPlacementInCode(PlacementInCode s) {
-        placementInCode = s;
+    public void addPlacementInCode(CtElement element) {
+        placementInCode = PlacementInCode.createPlacement(element);
+        annPosition = Utils.getFirstLJAnnotationPosition(element);
+    }
+
+    public void addPlacementInCode(PlacementInCode placement) {
+        placementInCode = placement;
     }
 
     public PlacementInCode getPlacementInCode() {
         return placementInCode;
     }
 
+    public SourcePosition getAnnPosition() {
+        return annPosition;
+    }
+
     @Override
     public int hashCode() {
         final int prime = 31;
@@ -65,4 +80,12 @@ public boolean equals(Object obj) {
             return supertypes.equals(other.supertypes);
         }
     }
+
+    public void setIsParameter(boolean b) {
+        isParameter = b;
+    }
+
+    public boolean isParameter() {
+        return isParameter;
+    }
 }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
index 052c6754..20c6079f 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
@@ -12,7 +12,6 @@
 import liquidjava.processor.facade.GhostDTO;
 import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker;
 import liquidjava.rj_language.Predicate;
-import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.utils.Utils;
 import spoon.reflect.code.CtLiteral;
 import spoon.reflect.cu.SourcePosition;
@@ -28,8 +27,8 @@
 import spoon.reflect.reference.CtTypeReference;
 
 public class ExternalRefinementTypeChecker extends TypeChecker {
-    String prefix;
-    Diagnostics diagnostics = Diagnostics.getInstance();
+    private String prefix;
+    private final Diagnostics diagnostics = Diagnostics.getInstance();
 
     public ExternalRefinementTypeChecker(Context context, Factory factory) {
         super(context, factory);
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
index d26cd25b..a91a4cb2 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
@@ -81,7 +81,7 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
         if (ref.isPresent()) {
             Predicate p = new Predicate(ref.get(), element);
             if (!p.getExpression().isBooleanExpression()) {
-                SourcePosition position = Utils.getAnnotationPosition(element, ref.get());
+                SourcePosition position = Utils.getLJAnnotationPosition(element, ref.get());
                 throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression",
                         ref.get());
             }
@@ -152,7 +152,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
                 CtLiteral<String> s = (CtLiteral<String>) ce;
                 String f = s.getValue();
                 GhostState gs = new GhostState(f, g.getParametersTypes(), factory.Type().BOOLEAN_PRIMITIVE,
-                        g.getPrefix());
+                        g.getPrefix(), Utils.getFile(element));
                 gs.setGhostParent(g);
                 gs.setRefinement(Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Types.INT)));
                 // open(THIS) -> state1(THIS) == 1
@@ -189,7 +189,7 @@ private void createStateGhost(String string, CtElement element, SourcePosition p
         List<CtTypeReference<?>> param = Collections.singletonList(factory.Type().createReference(qn));
 
         CtTypeReference<?> r = factory.Type().createReference(gd.returnType());
-        GhostState gs = new GhostState(gd.name(), param, r, qn);
+        GhostState gs = new GhostState(gd.name(), param, r, qn, Utils.getFile(element));
         context.addToGhostClass(sn, gs);
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java
index af16bf92..1f1decda 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java
@@ -154,6 +154,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
                 c = oc.get().substituteVariable(Keys.WILDCARD, paramName);
             param.putMetadata(Keys.REFINEMENT, c);
             RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c, param);
+            v.setIsParameter(true);
             rtc.getMessageFromAnnotation(param).ifPresent(v::setMessage);
             if (v instanceof Variable)
                 f.addArgRefinements((Variable) v);
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
index 61e2592c..bd35a3ee 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
@@ -209,7 +209,7 @@ private static Predicate createStatePredicate(String value, String targetClass,
             boolean isTo, String prefix) throws LJError {
         Predicate p = new Predicate(value, e, prefix);
         if (!p.getExpression().isBooleanExpression()) {
-            SourcePosition position = Utils.getAnnotationPosition(e, value);
+            SourcePosition position = Utils.getLJAnnotationPosition(e, value);
             throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression",
                     value);
         }
@@ -417,7 +417,7 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
                 .changeOldMentions(vi.getName(), instanceName);
 
         if (!tc.checkStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition
-            tc.throwStateRefinementError(fw.getPosition(), prevState, stateChange.getFrom(), stateChange.getMessage());
+            tc.throwStateRefinementError(fw.getPosition(), prevState, expectState, stateChange.getMessage());
             return;
         }
 
@@ -465,6 +465,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
                 .substituteVariable(name, instanceName);
 
         boolean found = false;
+        String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
         for (ObjectState stateChange : stateChanges) { // TODO: only working for 1 state annotation
             if (found) {
                 break;
@@ -482,8 +483,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
             expectState = expectState.changeOldMentions(vi.getName(), instanceName);
 
             found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition());
-            if (found && stateChange.hasTo()) {
-                String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
+            if (stateChange.hasTo()) {
                 Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, newInstanceName)
                         .substituteVariable(Keys.THIS, newInstanceName);
                 for (String s : map.keySet()) {
@@ -492,13 +492,17 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
                 transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName);
                 // update of state of new instance of this#n#(whatever it was + 1)
                 addInstanceWithState(tc, name, newInstanceName, vi, transitionedState, invocation);
-                return;
             }
         }
         if (!found) { // Reaches the end of stateChange no matching states
             Predicate expectedStatesDisjunction = stateChanges.stream().filter(ObjectState::hasFrom)
                     .map(ObjectState::getFrom)
                     .reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction);
+            expectedStatesDisjunction = expectedStatesDisjunction.substituteVariable(Keys.THIS, newInstanceName);
+            for (String s : map.keySet()) {
+                expectedStatesDisjunction = expectedStatesDisjunction.substituteVariable(s, map.get(s));
+            }
+            expectedStatesDisjunction = expectedStatesDisjunction.changeOldMentions(vi.getName(), newInstanceName);
 
             // combine messages of all state changes
             String message = stateChanges.stream().map(ObjectState::getMessage)
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
index cb3b0077..c91380ee 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
@@ -6,9 +6,7 @@
 import java.util.Map;
 import java.util.stream.Collectors;
 
-import liquidjava.diagnostics.errors.ArgumentMismatchError;
 import liquidjava.diagnostics.errors.LJError;
-import liquidjava.diagnostics.errors.SyntaxError;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostFunction;
@@ -88,7 +86,7 @@ protected Expression parse(String ref, CtElement element) throws LJError {
             return RefinementsParser.createAST(ref, prefix);
         } catch (LJError e) {
             // add location info to error
-            SourcePosition pos = Utils.getAnnotationPosition(element, ref);
+            SourcePosition pos = Utils.getLJAnnotationPosition(element, ref);
             e.setPosition(pos);
             throw e;
         }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
index 96f32f66..ef50bf7c 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
@@ -6,7 +6,6 @@
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.FPExpr;
 import com.microsoft.z3.FuncDecl;
-import com.microsoft.z3.FuncInterp;
 import com.microsoft.z3.IntExpr;
 import com.microsoft.z3.IntNum;
 import com.microsoft.z3.RealExpr;
diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java
index 1e99e3f0..82d37107 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java
@@ -38,12 +38,29 @@ public static String qualifyName(String prefix, String name) {
         return String.format("%s.%s", prefix, name);
     }
 
-    public static SourcePosition getAnnotationPosition(CtElement element, String refinement) {
+    public static String getFile(CtElement element) {
+        SourcePosition pos = element.getPosition();
+        if (pos == null || pos.getFile() == null)
+            return null;
+
+        return pos.getFile().getAbsolutePath();
+    }
+
+    public static SourcePosition getLJAnnotationPosition(CtElement element, String refinement) {
         return element.getAnnotations().stream()
                 .filter(a -> isLiquidJavaAnnotation(a) && hasRefinementValue(a, "\"" + refinement + "\"")).findFirst()
                 .map(CtElement::getPosition).orElse(element.getPosition());
     }
 
+    public static SourcePosition getFirstLJAnnotationPosition(CtElement element) {
+        return element.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation).map(CtElement::getPosition)
+                .min((p1, p2) -> {
+                    if (p1.getLine() != p2.getLine())
+                        return Integer.compare(p1.getLine(), p2.getLine());
+                    return Integer.compare(p1.getColumn(), p2.getColumn());
+                }).orElse(element.getPosition());
+    }
+
     private static boolean isLiquidJavaAnnotation(CtAnnotation<?> annotation) {
         return annotation.getAnnotationType().getQualifiedName().startsWith("liquidjava.specification");
     }