diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/logging/LogElement.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/logging/LogElement.java
new file mode 100644
index 00000000..56a7721e
--- /dev/null
+++ b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/logging/LogElement.java
@@ -0,0 +1,177 @@
+package liquidjava.logging;
+
+import liquidjava.processor.context.PlacementInCode;
+import spoon.reflect.code.CtComment;
+import spoon.reflect.code.CtInvocation;
+import spoon.reflect.cu.SourcePosition;
+import spoon.reflect.declaration.CtAnnotation;
+import spoon.reflect.declaration.CtElement;
+import spoon.reflect.declaration.ParentNotInitializedException;
+import spoon.reflect.path.CtPath;
+import spoon.reflect.path.CtRole;
+import spoon.reflect.reference.CtTypeReference;
+import spoon.reflect.visitor.Filter;
+
+import java.lang.annotation.Annotation;
+import java.lang.annotation.ElementType;
+import java.util.*;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+public class LogElement {
+    final private CtElement elem;
+
+    public LogElement(CtElement elem) {
+        this.elem = elem;
+    }
+
+    public <A extends Annotation> A getAnnotation(Class<A> var1) {
+        return elem.getAnnotation(var1);
+    }
+
+    public <A extends Annotation> boolean hasAnnotation(Class<A> var1) {
+        return elem.hasAnnotation(var1);
+    }
+
+    public List<CtAnnotation<? extends Annotation>> getAnnotations() {
+        return elem.getAnnotations();
+    }
+
+    public String getDocComment() {
+        return elem.getDocComment();
+    }
+
+    public String getShortRepresentation() {
+        return elem.getShortRepresentation();
+    }
+
+    public SourcePosition getPosition() {
+        return elem.getPosition();
+    }
+
+    public List<LogElement> getAnnotatedChildren(Class<? extends Annotation> var1) {
+        return elem.getAnnotatedChildren(var1).stream().map(LogElement::new).collect(Collectors.toList());
+    }
+
+    public boolean isImplicit() {
+        return elem.isImplicit();
+    }
+
+    public Set<CtTypeReference<?>> getReferencedTypes() {
+        return elem.getReferencedTypes();
+    }
+
+    public <E extends CtElement> List<LogElement> getElements(Filter<E> var1) {
+        return elem.getElements(var1).stream().map(LogElement::new).collect(Collectors.toList());
+    }
+
+    public LogElement getParent() throws ParentNotInitializedException {
+        return new LogElement(elem.getParent());
+    }
+
+    public <P extends CtElement> LogElement getParent(Class<P> var1) throws ParentNotInitializedException {
+        return new LogElement(elem.getParent(var1));
+    }
+
+    public <E extends CtElement> LogElement getParent(Filter<E> var1) throws ParentNotInitializedException {
+        return new LogElement(elem.getParent(var1));
+    }
+
+    public boolean isParentInitialized() {
+        return elem.isParentInitialized();
+    }
+
+    public boolean hasParent(LogElement var1) {
+        return elem.hasParent(var1.elem);
+    }
+
+    public CtRole getRoleInParent() {
+        return elem.getRoleInParent();
+    }
+
+    public Map<String, Object> getAllMetadata() {
+        return elem.getAllMetadata();
+    }
+
+    public Set<String> getMetadataKeys() {
+        return elem.getMetadataKeys();
+    }
+
+    public List<CtComment> getComments() {
+        return elem.getComments();
+    }
+
+    public <T> T getValueByRole(CtRole var1) {
+        return elem.getValueByRole(var1);
+    }
+
+    public CtPath getPath() {
+        return elem.getPath();
+    }
+
+    public Iterator<LogElement> descendantIterator() {
+        return new Iterator<LogElement>() {
+            final Iterator<CtElement> elemIt = elem.descendantIterator();
+
+            @Override
+            public boolean hasNext() {
+                return elemIt.hasNext();
+            }
+
+            @Override
+            public LogElement next() {
+                return new LogElement(elemIt.next());
+            }
+        };
+    }
+
+    public Iterable<LogElement> asIterable() {
+        return new Iterable<LogElement>() {
+            final Iterable<CtElement> elemIterable = elem.asIterable();
+
+            @Override
+            public Iterator<LogElement> iterator() {
+                return new Iterator<LogElement>() {
+                    final Iterator<CtElement> elemIt = elemIterable.iterator();
+
+                    @Override
+                    public boolean hasNext() {
+                        return elemIt.hasNext();
+                    }
+
+                    @Override
+                    public LogElement next() {
+                        return new LogElement(elemIt.next());
+                    }
+                };
+            }
+        };
+    }
+
+    public LogElement strippedElement() {
+        CtElement elemCopy = elem.clone();
+        // cleanup annotations
+        if (elem.getAnnotations().size() > 0) {
+            for (CtAnnotation<? extends Annotation> a : elem.getAnnotations()) {
+                elemCopy.removeAnnotation(a);
+            }
+        }
+        // cleanup comments
+        if (elem.getComments().size() > 0) {
+            for (CtComment a : elem.getComments()) {
+                elemCopy.removeComment(a);
+            }
+        }
+        return new LogElement(elemCopy);
+    }
+
+    public String toString() {
+        return elem.toString();
+    }
+
+    public Optional<String> inspectInvocation(Function<CtInvocation<?>, String> insperctor){
+        return elem instanceof CtInvocation<?> ?
+            Optional.of(insperctor.apply((CtInvocation<?>) elem)) :
+            Optional.empty();
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java
index f6681932..a1e62ed3 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java
@@ -3,11 +3,12 @@
 import java.util.Formatter;
 import java.util.HashMap;
 import java.util.Locale;
+
+import liquidjava.logging.LogElement;
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.PlacementInCode;
 import liquidjava.rj_language.Predicate;
 import spoon.reflect.code.CtLiteral;
-import spoon.reflect.declaration.CtElement;
 
 public class ErrorHandler {
 
@@ -16,16 +17,15 @@ public class ErrorHandler {
      *
      * @param <T>
      * @param var
-     * @param s
      * @param expectedType
      * @param cSMT
      */
-    public static <T> void printError(CtElement var, Predicate expectedType, Predicate cSMT,
+    public static <T> void printError(LogElement var, Predicate expectedType, Predicate cSMT,
             HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
         printError(var, null, expectedType, cSMT, map, ee);
     }
 
-    public static <T> void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
+    public static <T> void printError(LogElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
             HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
         String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +
         // cSMT.toString();
@@ -49,7 +49,7 @@ public static <T> void printError(CtElement var, String moreInfo, Predicate expe
         errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map);
     }
 
-    public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg,
+    public static void printStateMismatch(LogElement element, String method, VCImplication constraintForErrorMsg,
             String states, HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
 
         String resumeMessage = "Failed to check state transitions. " + "Expected possible states:" + states; // + ";
@@ -78,7 +78,7 @@ public static void printStateMismatch(CtElement element, String method, VCImplic
         errorl.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map);
     }
 
-    public static <T> void printErrorUnknownVariable(CtElement var, String et, String correctRefinement,
+    public static <T> void printErrorUnknownVariable(LogElement var, String et, String correctRefinement,
             HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
 
         String resumeMessage = "Encountered unknown variable";
@@ -97,7 +97,7 @@ public static <T> void printErrorUnknownVariable(CtElement var, String et, Strin
         errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map);
     }
 
-    public static <T> void printNotFound(CtElement var, Predicate constraint, Predicate constraint2, String msg,
+    public static <T> void printNotFound(LogElement var, Predicate constraint, Predicate constraint2, String msg,
             HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
 
         StringBuilder sb = new StringBuilder();
@@ -114,7 +114,7 @@ public static <T> void printNotFound(CtElement var, Predicate constraint, Predic
         errorl.addError(msg, sb.toString(), var.getPosition(), 2, map);
     }
 
-    public static <T> void printErrorArgs(CtElement var, Predicate expectedType, String msg,
+    public static <T> void printErrorArgs(LogElement var, Predicate expectedType, String msg,
             HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
@@ -128,7 +128,7 @@ public static <T> void printErrorArgs(CtElement var, Predicate expectedType, Str
         errorl.addError(title, sb.toString(), var.getPosition(), 2, map);
     }
 
-    public static void printErrorTypeMismatch(CtElement element, Predicate expectedType, String message,
+    public static void printErrorTypeMismatch(LogElement element, Predicate expectedType, String message,
             HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
@@ -141,7 +141,7 @@ public static void printErrorTypeMismatch(CtElement element, Predicate expectedT
         errorl.addError(message, sb.toString(), element.getPosition(), 2, map);
     }
 
-    public static void printSameStateSetError(CtElement element, Predicate p, String name,
+    public static void printSameStateSetError(LogElement element, Predicate p, String name,
             HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
         String resume = "Error found multiple disjoint states from a State Set in a refinement";
 
@@ -160,7 +160,7 @@ public static void printSameStateSetError(CtElement element, Predicate p, String
         errorl.addError(resume, sb.toString(), element.getPosition(), 1, map);
     }
 
-    public static void printErrorConstructorFromState(CtElement element, CtLiteral<String> from, ErrorEmitter errorl) {
+    public static void printErrorConstructorFromState(LogElement element, CtLiteral<String> from, ErrorEmitter errorl) {
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
         String s = " Error found constructor with FROM state (Constructor's should only have a TO state)\n\n";
@@ -173,7 +173,7 @@ public static void printErrorConstructorFromState(CtElement element, CtLiteral<S
         errorl.addError(s, sb.toString(), element.getPosition(), 1);
     }
 
-    public static void printCostumeError(CtElement element, String msg, ErrorEmitter errorl) {
+    public static void printCostumeError(LogElement element, String msg, ErrorEmitter errorl) {
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
         String s = "Found Error: " + msg;
@@ -186,7 +186,7 @@ public static void printCostumeError(CtElement element, String msg, ErrorEmitter
         errorl.addError(s, sb.toString(), element.getPosition(), 1);
     }
 
-    public static void printSyntaxError(String msg, String ref, CtElement element, ErrorEmitter errorl) {
+    public static void printSyntaxError(String msg, String ref, LogElement element, ErrorEmitter errorl) {
         StringBuilder sb = new StringBuilder();
         sb.append("______________________________________________________\n");
         StringBuilder sbtitle = new StringBuilder();
diff --git a/liquidjava-verifier/src/main/java/liquidjava/logging/LogElement.java b/liquidjava-verifier/src/main/java/liquidjava/logging/LogElement.java
new file mode 100644
index 00000000..0880c7a1
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/logging/LogElement.java
@@ -0,0 +1,174 @@
+package liquidjava.logging;
+
+import spoon.reflect.code.CtComment;
+import spoon.reflect.code.CtInvocation;
+import spoon.reflect.cu.SourcePosition;
+import spoon.reflect.declaration.CtAnnotation;
+import spoon.reflect.declaration.CtElement;
+import spoon.reflect.declaration.ParentNotInitializedException;
+import spoon.reflect.path.CtPath;
+import spoon.reflect.path.CtRole;
+import spoon.reflect.reference.CtTypeReference;
+import spoon.reflect.visitor.Filter;
+
+import java.lang.annotation.Annotation;
+import java.util.*;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+public class LogElement {
+    final private CtElement elem;
+
+    public LogElement(CtElement elem) {
+        this.elem = elem;
+    }
+
+    public <A extends Annotation> A getAnnotation(Class<A> var1) {
+        return elem.getAnnotation(var1);
+    }
+
+    public <A extends Annotation> boolean hasAnnotation(Class<A> var1) {
+        return elem.hasAnnotation(var1);
+    }
+
+    public List<CtAnnotation<? extends Annotation>> getAnnotations() {
+        return elem.getAnnotations();
+    }
+
+    public String getDocComment() {
+        return elem.getDocComment();
+    }
+
+    public String getShortRepresentation() {
+        return elem.getShortRepresentation();
+    }
+
+    public SourcePosition getPosition() {
+        return elem.getPosition();
+    }
+
+    public List<LogElement> getAnnotatedChildren(Class<? extends Annotation> var1) {
+        return elem.getAnnotatedChildren(var1).stream().map(LogElement::new).collect(Collectors.toList());
+    }
+
+    public boolean isImplicit() {
+        return elem.isImplicit();
+    }
+
+    public Set<CtTypeReference<?>> getReferencedTypes() {
+        return elem.getReferencedTypes();
+    }
+
+    public <E extends CtElement> List<LogElement> getElements(Filter<E> var1) {
+        return elem.getElements(var1).stream().map(LogElement::new).collect(Collectors.toList());
+    }
+
+    public LogElement getParent() throws ParentNotInitializedException {
+        return new LogElement(elem.getParent());
+    }
+
+    public <P extends CtElement> LogElement getParent(Class<P> var1) throws ParentNotInitializedException {
+        return new LogElement(elem.getParent(var1));
+    }
+
+    public <E extends CtElement> LogElement getParent(Filter<E> var1) throws ParentNotInitializedException {
+        return new LogElement(elem.getParent(var1));
+    }
+
+    public boolean isParentInitialized() {
+        return elem.isParentInitialized();
+    }
+
+    public boolean hasParent(LogElement var1) {
+        return elem.hasParent(var1.elem);
+    }
+
+    public CtRole getRoleInParent() {
+        return elem.getRoleInParent();
+    }
+
+    public Map<String, Object> getAllMetadata() {
+        return elem.getAllMetadata();
+    }
+
+    public Set<String> getMetadataKeys() {
+        return elem.getMetadataKeys();
+    }
+
+    public List<CtComment> getComments() {
+        return elem.getComments();
+    }
+
+    public <T> T getValueByRole(CtRole var1) {
+        return elem.getValueByRole(var1);
+    }
+
+    public CtPath getPath() {
+        return elem.getPath();
+    }
+
+    public Iterator<LogElement> descendantIterator() {
+        return new Iterator<LogElement>() {
+            final Iterator<CtElement> elemIt = elem.descendantIterator();
+
+            @Override
+            public boolean hasNext() {
+                return elemIt.hasNext();
+            }
+
+            @Override
+            public LogElement next() {
+                return new LogElement(elemIt.next());
+            }
+        };
+    }
+
+    public Iterable<LogElement> asIterable() {
+        return new Iterable<LogElement>() {
+            final Iterable<CtElement> elemIterable = elem.asIterable();
+
+            @Override
+            public Iterator<LogElement> iterator() {
+                return new Iterator<LogElement>() {
+                    final Iterator<CtElement> elemIt = elemIterable.iterator();
+
+                    @Override
+                    public boolean hasNext() {
+                        return elemIt.hasNext();
+                    }
+
+                    @Override
+                    public LogElement next() {
+                        return new LogElement(elemIt.next());
+                    }
+                };
+            }
+        };
+    }
+
+    public LogElement strippedElement() {
+        CtElement elemCopy = elem.clone();
+        // cleanup annotations
+        if (elem.getAnnotations().size() > 0) {
+            for (CtAnnotation<? extends Annotation> a : elem.getAnnotations()) {
+                elemCopy.removeAnnotation(a);
+            }
+        }
+        // cleanup comments
+        if (elem.getComments().size() > 0) {
+            for (CtComment a : elem.getComments()) {
+                elemCopy.removeComment(a);
+            }
+        }
+        return new LogElement(elemCopy);
+    }
+
+    public String toString() {
+        return elem.toString();
+    }
+
+    public Optional<String> inspectInvocation(Function<CtInvocation<?>, String> insperctor) {
+        return elem instanceof CtInvocation<?> ? Optional.of(insperctor.apply((CtInvocation<?>) elem))
+                : Optional.empty();
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java
index 6b149ca9..f96843a4 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java
@@ -5,6 +5,7 @@
 import java.util.List;
 import java.util.Map;
 import liquidjava.errors.ErrorEmitter;
+import liquidjava.logging.LogElement;
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
@@ -59,7 +60,7 @@ public Expression getNewExpression(List<String> newNames) {
         return expr.getExpression().clone();
     }
 
-    public Predicate getPremises(List<String> list, List<String> newNames, CtElement elem, ErrorEmitter ee)
+    public Predicate getPremises(List<String> list, List<String> newNames, LogElement elem, ErrorEmitter ee)
             throws ParsingException {
         List<Predicate> invocationPredicates = getPredicatesFromExpression(list, elem, ee);
         Predicate prem = new Predicate();
@@ -70,7 +71,7 @@ public Predicate getPremises(List<String> list, List<String> newNames, CtElement
         return prem.clone();
     }
 
-    private List<Predicate> getPredicatesFromExpression(List<String> list, CtElement elem, ErrorEmitter ee)
+    private List<Predicate> getPredicatesFromExpression(List<String> list, LogElement elem, ErrorEmitter ee)
             throws ParsingException {
         List<Predicate> lp = new ArrayList<>();
         for (String e : list)
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 d604a00d..021745d0 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
@@ -1,6 +1,8 @@
 package liquidjava.processor.context;
 
 import java.util.*;
+
+import liquidjava.logging.LogElement;
 import liquidjava.rj_language.Predicate;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.reference.CtTypeReference;
@@ -116,7 +118,7 @@ public void addVarToContext(RefinedVariable var) {
     }
 
     public RefinedVariable addVarToContext(String simpleName, CtTypeReference<?> type, Predicate c,
-            CtElement placementInCode) {
+            LogElement placementInCode) {
         RefinedVariable vi = new Variable(simpleName, type, c);
         vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode));
         vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
@@ -125,7 +127,7 @@ public RefinedVariable addVarToContext(String simpleName, CtTypeReference<?> typ
     }
 
     public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference<?> type, Predicate c,
-            CtElement placementInCode) {
+            LogElement placementInCode) {
         RefinedVariable vi = new VariableInstance(simpleName, type, c);
         vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode));
         if (!ctxSpecificVars.contains(vi))
@@ -134,7 +136,7 @@ public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference<?
     }
 
     public void addRefinementToVariableInContext(String name, CtTypeReference<?> type, Predicate et,
-            CtElement placementInCode) {
+            LogElement placementInCode) {
         if (hasVariable(name)) {
             RefinedVariable vi = getVariableByName(name);
             vi.setRefinement(et);
@@ -248,7 +250,8 @@ public void addSpecificVariable(RefinedVariable vi) {
         }
     }
 
-    // ---------------------- Variables - if information storing ----------------------
+    // ---------------------- Variables - if information storing
+    // ----------------------
     public void variablesSetBeforeIf() {
         for (RefinedVariable vi : getAllVariables())
             if (vi instanceof Variable)
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java
index 2a8f90af..e92fdceb 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java
@@ -1,6 +1,8 @@
 package liquidjava.processor.context;
 
 import java.lang.annotation.Annotation;
+
+import liquidjava.logging.LogElement;
 import spoon.reflect.code.CtComment;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtAnnotation;
@@ -31,21 +33,8 @@ public void setPosition(SourcePosition position) {
         this.position = position;
     }
 
-    public static PlacementInCode createPlacement(CtElement elem) {
-        CtElement elemCopy = elem.clone();
-        // cleanup annotations
-        if (elem.getAnnotations().size() > 0) {
-            for (CtAnnotation<? extends Annotation> a : elem.getAnnotations()) {
-                elemCopy.removeAnnotation(a);
-            }
-        }
-        // cleanup comments
-        if (elem.getComments().size() > 0) {
-            for (CtComment a : elem.getComments()) {
-                elemCopy.removeComment(a);
-            }
-        }
-        String elemText = elemCopy.toString();
+    public static PlacementInCode createPlacement(LogElement elem) {
+        String elemText = elem.strippedElement().toString();
         return new PlacementInCode(elemText, elem.getPosition());
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java
index b7d6b07c..086e7954 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java
@@ -3,6 +3,8 @@
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Optional;
+
+import liquidjava.logging.LogElement;
 import liquidjava.rj_language.Predicate;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.reference.CtTypeReference;
@@ -47,11 +49,11 @@ public String getTargetClass() {
         return targetClass;
     }
 
-    public Predicate getRenamedRefinements(Context c, CtElement element) {
+    public Predicate getRenamedRefinements(Context c, LogElement element) {
         return getRenamedRefinements(getAllRefinements(), c, element);
     }
 
-    private Predicate getRenamedRefinements(Predicate place, Context context, CtElement element) {
+    private Predicate getRenamedRefinements(Predicate place, Context context, LogElement element) {
         Predicate update = place.clone();
         for (Variable p : argRefinements) {
             String varName = p.getName();
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 fe8de3c5..985ad459 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
@@ -5,6 +5,7 @@
 import java.util.Optional;
 import liquidjava.errors.ErrorEmitter;
 import liquidjava.errors.ErrorHandler;
+import liquidjava.logging.LogElement;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostFunction;
 import liquidjava.processor.facade.GhostDTO;
@@ -96,8 +97,8 @@ protected void getGhostFunction(String value, CtElement element) {
             }
 
         } catch (ParsingException e) {
-            ErrorHandler.printCostumeError(element, "Could not parse the Ghost Function" + e.getMessage(),
-                    errorEmitter);
+            ErrorHandler.printCostumeError(new LogElement(element),
+                    "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
             // e.printStackTrace();
         }
     }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
index e798214f..27245fdc 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
@@ -8,6 +8,8 @@
 import org.apache.commons.lang3.NotImplementedException;
 
 import liquidjava.errors.ErrorEmitter;
+import liquidjava.errors.ErrorHandler;
+import liquidjava.logging.LogElement;
 import liquidjava.processor.context.*;
 import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker;
 import liquidjava.processor.refinement_checker.general_checkers.OperationsChecker;
@@ -133,7 +135,7 @@ public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
                 return; // error already in ErrorEmitter
             }
             context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()),
-                    localVariable);
+                    new LogElement(localVariable));
         } else {
             String varName = localVariable.getSimpleName();
             CtExpression<?> e = localVariable.getAssignment();
@@ -142,7 +144,7 @@ public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
             if (refinementFound == null) {
                 refinementFound = new Predicate();
             }
-            context.addVarToContext(varName, localVariable.getType(), new Predicate(), e);
+            context.addVarToContext(varName, localVariable.getType(), new Predicate(), new LogElement(e));
 
             try {
                 checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable,
@@ -177,11 +179,11 @@ public <T> void visitCtNewArray(CtNewArray<T> newArray) {
             } else {
                 c = Predicate.createEquals(Predicate.createVar(name), c);
             }
-            context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, exp);
+            context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, new LogElement(exp));
             Predicate ep;
             try {
                 ep = Predicate.createEquals(
-                        BuiltinFunctionPredicate.builtin_length(WILD_VAR, newArray, getErrorEmitter()),
+                        BuiltinFunctionPredicate.builtin_length(WILD_VAR, new LogElement(newArray), getErrorEmitter()),
                         Predicate.createVar(name));
             } catch (ParsingException e) {
                 return; // error already in ErrorEmitter
@@ -249,7 +251,7 @@ public <T> void visitCtArrayRead(CtArrayRead<T> arrayRead) {
 
         super.visitCtArrayRead(arrayRead);
         String name = String.format(instanceFormat, "arrayAccess", context.getCounter());
-        context.addVarToContext(name, arrayRead.getType(), new Predicate(), arrayRead);
+        context.addVarToContext(name, arrayRead.getType(), new Predicate(), new LogElement(arrayRead));
         arrayRead.putMetadata(REFINE_KEY, Predicate.createVar(name));
         // TODO predicate for now is always TRUE
     }
@@ -295,7 +297,7 @@ public <T> void visitCtField(CtField<T> f) {
         if (c.isPresent()) {
             ret = c.get().substituteVariable(WILD_VAR, nname).substituteVariable(f.getSimpleName(), nname);
         }
-        RefinedVariable v = context.addVarToContext(nname, f.getType(), ret, f);
+        RefinedVariable v = context.addVarToContext(nname, f.getType(), ret, new LogElement(f));
         if (v instanceof Variable) {
             ((Variable) v).setLocation("this");
         }
@@ -326,8 +328,9 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
         } else if (fieldRead.getVariable().getSimpleName().equals("length")) {
             String targetName = fieldRead.getTarget().toString();
             try {
-                fieldRead.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR),
-                        BuiltinFunctionPredicate.builtin_length(targetName, fieldRead, getErrorEmitter())));
+                fieldRead.putMetadata(REFINE_KEY,
+                        Predicate.createEquals(Predicate.createVar(WILD_VAR), BuiltinFunctionPredicate
+                                .builtin_length(targetName, new LogElement(fieldRead), getErrorEmitter())));
             } catch (ParsingException e) {
                 return; // error already in ErrorEmitter
             }
@@ -425,7 +428,7 @@ public void visitCtIf(CtIf ifElement) {
         }
 
         RefinedVariable freshRV = context.addInstanceToContext(freshVarName, factory.Type().INTEGER_PRIMITIVE, expRefs,
-                exp);
+                new LogElement(exp));
         vcChecker.addPathVariable(freshRV);
 
         context.variablesNewIfCombination();
@@ -467,7 +470,7 @@ public <T> void visitCtArrayWrite(CtArrayWrite<T> arrayWrite) {
         BuiltinFunctionPredicate fp;
         try {
             fp = BuiltinFunctionPredicate.builtin_addToIndex(arrayWrite.getTarget().toString(), index.toString(),
-                    WILD_VAR, arrayWrite, getErrorEmitter());
+                    WILD_VAR, new LogElement(arrayWrite), getErrorEmitter());
         } catch (ParsingException e) {
             return; // error already in ErrorEmitter
         }
@@ -547,7 +550,7 @@ private Predicate getExpressionRefinements(CtExpression<?> element) throws Parsi
             return getRefinement(op);
         } else if (element instanceof CtLiteral<?>) {
             CtLiteral<?> l = (CtLiteral<?>) element;
-            return new Predicate(l.getValue().toString(), l, errorEmitter);
+            return new Predicate(l.getValue().toString(), new LogElement(l), errorEmitter);
         } else if (element instanceof CtInvocation<?>) {
             CtInvocation<?> inv = (CtInvocation<?>) element;
             visitCtInvocation(inv);
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 9369cb8a..7b456492 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
@@ -6,6 +6,7 @@
 import java.util.Optional;
 import liquidjava.errors.ErrorEmitter;
 import liquidjava.errors.ErrorHandler;
+import liquidjava.logging.LogElement;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostFunction;
@@ -86,7 +87,7 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
             }
         }
         if (ref.isPresent()) {
-            Predicate p = new Predicate(ref.get(), element, errorEmitter);
+            Predicate p = new Predicate(ref.get(), new LogElement(element), errorEmitter);
             if (errorEmitter.foundError())
                 return Optional.empty();
             constr = Optional.of(p);
@@ -147,11 +148,12 @@ private void createStateGhost(String string, CtAnnotation<? extends Annotation>
         try {
             gd = RefinementsParser.getGhostDeclaration(string);
         } catch (ParsingException e) {
-            ErrorHandler.printCostumeError(ann, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
+            ErrorHandler.printCostumeError(new LogElement(ann), "Could not parse the Ghost Function" + e.getMessage(),
+                    errorEmitter);
             return;
         }
         if (gd.getParam_types().size() > 0) {
-            ErrorHandler.printCostumeError(ann, "Ghost States have the class as parameter "
+            ErrorHandler.printCostumeError(new LogElement(ann), "Ghost States have the class as parameter "
                     + "by default, no other parameters are allowed in '" + string + "'", errorEmitter);
             return;
         }
@@ -211,8 +213,8 @@ protected void getGhostFunction(String value, CtElement element) {
                 context.addGhostFunction(gh);
             }
         } catch (ParsingException e) {
-            ErrorHandler.printCostumeError(element, "Could not parse the Ghost Function" + e.getMessage(),
-                    errorEmitter);
+            ErrorHandler.printCostumeError(new LogElement(element),
+                    "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
             // e.printStackTrace();
             return;
         }
@@ -238,7 +240,7 @@ protected void handleAlias(String value, CtElement element) {
                 }
             }
         } catch (ParsingException e) {
-            ErrorHandler.printCostumeError(element, e.getMessage(), errorEmitter);
+            ErrorHandler.printCostumeError(new LogElement(element), e.getMessage(), errorEmitter);
             return;
             // e.printStackTrace();
         }
@@ -280,39 +282,40 @@ else if (expectedType.isPresent())
         cEt = cEt.substituteVariable(simpleName, newName);
 
         // Substitute variable in verification
-        RefinedVariable rv = context.addInstanceToContext(newName, type, correctNewRefinement, usage);
+        RefinedVariable rv = context.addInstanceToContext(newName, type, correctNewRefinement, new LogElement(usage));
         for (CtTypeReference<?> t : mainRV.getSuperTypes())
             rv.addSuperType(t);
         context.addRefinementInstanceToVariable(simpleName, newName);
         // smt check
-        checkSMT(cEt, usage); // TODO CHANGE
-        context.addRefinementToVariableInContext(simpleName, type, cet, usage);
+        checkSMT(cEt, usage);// TODO CHANGE
+        context.addRefinementToVariableInContext(simpleName, type, cet, new LogElement(usage));
     }
 
     public void checkSMT(Predicate expectedType, CtElement element) {
-        vcChecker.processSubtyping(expectedType, context.getGhostState(), WILD_VAR, THIS, element, factory);
+        vcChecker.processSubtyping(expectedType, context.getGhostState(), WILD_VAR, THIS, new LogElement(element),
+                factory);
         element.putMetadata(REFINE_KEY, expectedType);
     }
 
-    public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String string) {
+    public void checkStateSMT(Predicate prevState, Predicate expectedState, LogElement target, String string) {
         vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, target, string,
                 factory);
     }
 
-    public boolean checksStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) {
+    public boolean checksStateSMT(Predicate prevState, Predicate expectedState, LogElement p) {
         return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, p,
                 factory);
     }
 
-    public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customeMessage) {
+    public void createError(LogElement element, Predicate expectedType, Predicate foundType, String customeMessage) {
         vcChecker.printSubtypingError(element, expectedType, foundType, customeMessage);
     }
 
-    public void createSameStateError(CtElement element, Predicate expectedType, String klass) {
+    public void createSameStateError(LogElement element, Predicate expectedType, String klass) {
         vcChecker.printSameStateError(element, expectedType, klass);
     }
 
-    public void createStateMismatchError(CtElement element, String method, Predicate c, String states) {
+    public void createStateMismatchError(LogElement element, String method, Predicate c, String states) {
         vcChecker.printStateMismatchError(element, method, c, states);
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java
index 75ca4b94..cc9caf07 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java
@@ -8,6 +8,7 @@
 import java.util.stream.Collectors;
 import liquidjava.errors.ErrorEmitter;
 import liquidjava.errors.ErrorHandler;
+import liquidjava.logging.LogElement;
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.*;
 import liquidjava.rj_language.Predicate;
@@ -35,7 +36,7 @@ public VCChecker(ErrorEmitter errorEmitter) {
     }
 
     public void processSubtyping(Predicate expectedType, List<GhostState> list, String wild_var, String this_var,
-            CtElement element, Factory f) {
+            LogElement element, Factory f) {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(expectedType, lrv, mainVars);
         if (expectedType.isBooleanTrue())
@@ -65,14 +66,14 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, Stri
     }
 
     public void processSubtyping(Predicate type, Predicate expectedType, List<GhostState> list, String wild_var,
-            String this_var, CtElement element, String string, Factory f) {
-        boolean b = canProcessSubtyping(type, expectedType, list, wild_var, this_var, element.getPosition(), f);
+            String this_var, LogElement element, String string, Factory f) {
+        boolean b = canProcessSubtyping(type, expectedType, list, wild_var, this_var, element, f);
         if (!b)
             printSubtypingError(element, expectedType, type, string);
     }
 
     public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<GhostState> list, String wild_var,
-            String this_var, SourcePosition p, Factory f) {
+            String this_var, LogElement p, Factory f) {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(expectedType, lrv, mainVars);
         gatherVariables(type, lrv, mainVars);
@@ -203,7 +204,7 @@ private void recAuxGetVars(RefinedVariable var, List<RefinedVariable> newVars) {
         getVariablesFromContext(l, newVars, varName);
     }
 
-    public boolean smtChecks(Predicate cSMT, Predicate expectedType, SourcePosition p) {
+    public boolean smtChecks(Predicate cSMT, Predicate expectedType, LogElement p) {
         try {
             new SMTEvaluator().verifySubtype(cSMT, expectedType, context);
         } catch (TypeCheckError e) {
@@ -213,7 +214,7 @@ public boolean smtChecks(Predicate cSMT, Predicate expectedType, SourcePosition
             // e.printStackTrace();
             // System.exit(7);
             // fail();
-            errorEmitter.addError("Unknown Error", e.getMessage(), p, 7);
+            errorEmitter.addError("Unknown Error", e.getMessage(), p.getPosition(), 7);
         }
         return true;
     }
@@ -271,7 +272,7 @@ private void printVCs(String string, String stringSMT, Predicate expectedType) {
     // Print
     // Errors---------------------------------------------------------------------------------------------------
 
-    private HashMap<String, PlacementInCode> createMap(CtElement element, Predicate expectedType) {
+    private HashMap<String, PlacementInCode> createMap(LogElement element, Predicate expectedType) {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(expectedType, lrv, mainVars);
         HashMap<String, PlacementInCode> map = new HashMap<>();
@@ -279,7 +280,7 @@ private HashMap<String, PlacementInCode> createMap(CtElement element, Predicate
         return map;
     }
 
-    protected void printSubtypingError(CtElement element, Predicate expectedType, Predicate foundType,
+    protected void printSubtypingError(LogElement element, Predicate expectedType, Predicate foundType,
             String customeMsg) {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(expectedType, lrv, mainVars);
@@ -289,23 +290,21 @@ protected void printSubtypingError(CtElement element, Predicate expectedType, Pr
         printError(premises, expectedType, element, map, customeMsg);
     }
 
-    public void printSameStateError(CtElement element, Predicate expectedType, String klass) {
+    public void printSameStateError(LogElement element, Predicate expectedType, String klass) {
         HashMap<String, PlacementInCode> map = createMap(element, expectedType);
         ErrorHandler.printSameStateSetError(element, expectedType, klass, map, errorEmitter);
     }
 
-    private void printError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element,
+    private void printError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, LogElement element,
             HashMap<String, PlacementInCode> map) {
-        String s = null;
-        if (element instanceof CtInvocation) {
-            CtInvocation<?> ci = (CtInvocation<?>) element;
+        String s = element.inspectInvocation(ci -> {
             String totalS = ci.getExecutable().toString();
             if (ci.getTarget() != null) {
                 int targetL = ci.getTarget().toString().length();
                 totalS = ci.toString().substring(targetL + 1);
             }
-            s = "Method invocation " + totalS + " in:";
-        }
+            return "Method invocation " + totalS + " in:";
+        }).orElse(null);
 
         Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map);
         Predicate cSMTMessageReady = premisesBeforeChange; // substituteByMap(premisesBeforeChange, map);
@@ -325,14 +324,14 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e
         }
     }
 
-    private void printError(Predicate premises, Predicate expectedType, CtElement element,
+    private void printError(Predicate premises, Predicate expectedType, LogElement element,
             HashMap<String, PlacementInCode> map, String s) {
         Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map);
         Predicate cSMTMessageReady = premises; // substituteByMap(premises, map);
         ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter);
     }
 
-    public void printStateMismatchError(CtElement element, String method, Predicate c, String states) {
+    public void printStateMismatchError(LogElement element, String method, Predicate c, String states) {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(c, lrv, mainVars);
         HashMap<String, PlacementInCode> map = new HashMap<>();
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 d14efa15..f3cc7230 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
@@ -6,6 +6,8 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Optional;
+
+import liquidjava.logging.LogElement;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.RefinedFunction;
 import liquidjava.processor.context.RefinedVariable;
@@ -151,7 +153,8 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
             if (oc.isPresent())
                 c = oc.get().substituteVariable(rtc.WILD_VAR, paramName);
             param.putMetadata(rtc.REFINE_KEY, c);
-            RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c, param);
+            RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c,
+                    new LogElement(param));
             if (v instanceof Variable)
                 f.addArgRefinements((Variable) v);
             joint = Predicate.createConjunction(joint, c);
@@ -198,7 +201,7 @@ public <R> void getReturnRefinements(CtReturn<R> ret) {
 
                 // Both return and the method have metadata
                 String thisName = String.format(rtc.thisFormat, className);
-                rtc.getContext().addInstanceToContext(thisName, c.getReference(), new Predicate(), ret);
+                rtc.getContext().addInstanceToContext(thisName, c.getReference(), new Predicate(), new LogElement(ret));
 
                 String returnVarName = String.format(retNameFormat, rtc.getContext().getCounter());
                 Predicate cretRef = rtc.getRefinement(ret.getReturnedExpression())
@@ -206,7 +209,7 @@ public <R> void getReturnRefinements(CtReturn<R> ret) {
                 Predicate cexpectedType = fi.getRefReturn().substituteVariable(rtc.WILD_VAR, returnVarName)
                         .substituteVariable(rtc.THIS, returnVarName);
 
-                rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret);
+                rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, new LogElement(ret));
                 rtc.checkSMT(cexpectedType, ret);
                 rtc.getContext().newRefinementToVariableInContext(returnVarName, cexpectedType);
             }
@@ -314,7 +317,7 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
 
             String viName = String.format(rtc.instanceFormat, f.getName(), rtc.getContext().getCounter());
             VariableInstance vi = (VariableInstance) rtc.getContext().addInstanceToContext(viName, f.getType(),
-                    methodRef.substituteVariable(rtc.WILD_VAR, viName), invocation); // TODO REVER!!
+                    methodRef.substituteVariable(rtc.WILD_VAR, viName), new LogElement(invocation)); // TODO REVER!!
             if (varName != null && f.hasStateChange() && equalsThis)
                 rtc.getContext().addRefinementInstanceToVariable(varName, viName);
             invocation.putMetadata(rtc.TARGET_KEY, vi);
@@ -356,7 +359,8 @@ private String createVariableRepresentingArgument(CtExpression<?> iArg, Variable
         if (!met.getVariableNames().contains(rtc.WILD_VAR))
             met = Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), met);
         String nVar = String.format(rtc.instanceFormat, fArg.getName(), rtc.getContext().getCounter());
-        rtc.getContext().addInstanceToContext(nVar, fArg.getType(), met.substituteVariable(rtc.WILD_VAR, nVar), iArg);
+        rtc.getContext().addInstanceToContext(nVar, fArg.getType(), met.substituteVariable(rtc.WILD_VAR, nVar),
+                new LogElement(iArg));
         return nVar;
     }
 
@@ -378,7 +382,7 @@ private <R> void checkParameters(CtElement invocation, List<CtExpression<?>> arg
 
     // IN CONSTRUCTION _ NOT USED
     @SuppressWarnings("unused")
-    private void applyRefinementsToArguments(CtElement element, List<CtExpression<?>> arguments, RefinedFunction f,
+    private void applyRefinementsToArguments(LogElement element, List<CtExpression<?>> arguments, RefinedFunction f,
             Map<String, String> map) {
         Context context = rtc.getContext();
         List<CtExpression<?>> invocationParams = arguments;
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java
index 0ce0f318..3af8c7e7 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java
@@ -6,6 +6,7 @@
 
 import org.apache.commons.lang3.NotImplementedException;
 
+import liquidjava.logging.LogElement;
 import liquidjava.processor.context.RefinedFunction;
 import liquidjava.processor.context.RefinedVariable;
 import liquidjava.processor.context.Variable;
@@ -111,7 +112,7 @@ public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws Parsin
         if (ex instanceof CtVariableWrite) {
             CtVariableWrite<T> w = (CtVariableWrite<T>) ex;
             name = w.getVariable().getSimpleName();
-            all = getRefinementUnaryVariableWrite(ex, operator, w, name);
+            all = getRefinementUnaryVariableWrite(new LogElement(ex), operator, w, name);
             rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration());
             return;
 
@@ -125,7 +126,7 @@ public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws Parsin
                     CtVariableWrite<T> w = (CtVariableWrite<T>) assign.getAssigned();
                     String parentName = w.getVariable().getSimpleName();
                     if (name.equals(parentName)) {
-                        all = getRefinementUnaryVariableWrite(ex, operator, w, name);
+                        all = getRefinementUnaryVariableWrite(new LogElement(ex), operator, w, name);
                         operator.putMetadata(rtc.REFINE_KEY, all);
                         return;
                     }
@@ -143,7 +144,7 @@ public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws Parsin
             newName = String.format(name, rtc.getContext().getCounter());
         Predicate newMeta = metadata.substituteVariable(rtc.WILD_VAR, newName);
 
-        Predicate unOp = getOperatorFromKind(operator.getKind(), operator);
+        Predicate unOp = getOperatorFromKind(operator.getKind(), new LogElement(operator));
         CtElement p = operator.getParent();
         Predicate opS = unOp.substituteVariable(rtc.WILD_VAR, newName);
 
@@ -152,7 +153,7 @@ public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws Parsin
         else
             all = Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), opS); // TODO SEE IF () IN OPS IS NEEDED
 
-        rtc.getContext().addInstanceToContext(newName, ex.getType(), newMeta, operator);
+        rtc.getContext().addInstanceToContext(newName, ex.getType(), newMeta, new LogElement(operator));
         operator.putMetadata(rtc.REFINE_KEY, all);
     }
 
@@ -188,12 +189,14 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtExpres
      */
     private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariableWrite<?> parentVar,
             CtExpression<?> element) throws ParsingException {
+        LogElement elementForLogging = new LogElement(element);
+
         if (element instanceof CtFieldRead<?>) {
             CtFieldRead<?> field = ((CtFieldRead<?>) element);
             if (field.getVariable().getSimpleName().equals("length")) {
                 String name = String.format(rtc.freshFormat, rtc.getContext().getCounter());
                 rtc.getContext().addVarToContext(name, element.getType(),
-                        rtc.getRefinement(element).substituteVariable(rtc.WILD_VAR, name), field);
+                        rtc.getRefinement(element).substituteVariable(rtc.WILD_VAR, name), new LogElement(field));
                 return Predicate.createVar(name);
             }
         }
@@ -201,6 +204,7 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
         if (element instanceof CtVariableRead<?>) {
             CtVariableRead<?> elemVar = (CtVariableRead<?>) element;
             String elemName = elemVar.getVariable().getSimpleName();
+            LogElement elemVarForLogging = new LogElement(elemVar);
             if (elemVar instanceof CtFieldRead)
                 elemName = String.format(rtc.thisFormat, elemName);
             Predicate elem_ref = rtc.getContext().getVariableRefinements(elemName);
@@ -215,13 +219,13 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
                 Predicate newElem_ref = elem_ref.substituteVariable(rtc.WILD_VAR, newName);
                 // String newElem_ref = elem_ref.replace(rtc.WILD_VAR, newName);
                 RefinedVariable newVi = rtc.getContext().addVarToContext(newName, elemVar.getType(), newElem_ref,
-                        elemVar);
+                        elemVarForLogging);
                 rtc.getContext().addSpecificVariable(newVi);
                 returnName = newName;
             }
 
             Predicate e = elem_ref.substituteVariable(rtc.WILD_VAR, elemName);
-            rtc.getContext().addVarToContext(elemName, elemVar.getType(), e, elemVar);
+            rtc.getContext().addVarToContext(elemName, elemVar.getType(), e, elemVarForLogging);
             return Predicate.createVar(returnName);
         } else if (element instanceof CtBinaryOperator<?>) {
             CtBinaryOperator<?> binop = (CtBinaryOperator<?>) element;
@@ -234,13 +238,12 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
         } else if (element instanceof CtUnaryOperator<?>) {
             Predicate a = (Predicate) element.getMetadata(rtc.REFINE_KEY);
             a = a.substituteVariable(rtc.WILD_VAR, "");
-            String s = a.toString().replace("(", "").replace(")", "").replace("==", "").replace(" ", ""); // TODO
-            // IMPROVE
-            return new Predicate(String.format("(%s)", s), element, rtc.getErrorEmitter());
+            String s = a.toString().replace("(", "").replace(")", "").replace("==", "").replace(" ", "");// TODO IMPROVE
+            return new Predicate(String.format("(%s)", s), elementForLogging, rtc.getErrorEmitter());
 
         } else if (element instanceof CtLiteral<?>) {
             CtLiteral<?> l = (CtLiteral<?>) element;
-            return new Predicate(l.getValue().toString(), element, rtc.getErrorEmitter());
+            return new Predicate(l.getValue().toString(), elementForLogging, rtc.getErrorEmitter());
 
         } else if (element instanceof CtInvocation<?>) {
             CtInvocation<?> inv = (CtInvocation<?>) element;
@@ -252,13 +255,13 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
             // Get function refinements with non_used variables
             String met = ((CtClass<?>) method.getParent()).getQualifiedName(); // TODO check
             RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met);
-            Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVER!!
+            Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), elementForLogging);// TODO REVER!!
             // Substitute _ by the variable that we send
             String newName = String.format(rtc.freshFormat, rtc.getContext().getCounter());
 
             innerRefs = innerRefs.substituteVariable(rtc.WILD_VAR, newName);
-            rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv);
-            return new Predicate(newName, inv, rtc.getErrorEmitter()); // Return variable that represents the invocation
+            rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, elementForLogging);
+            return new Predicate(newName, elementForLogging, rtc.getErrorEmitter());// Return variable that represents
         }
         return rtc.getRefinement(element);
         // TODO Maybe add cases
@@ -268,6 +271,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv, CtB
             throws ParsingException {
 
         CtExpression<?> t = inv.getTarget();
+        LogElement logging = new LogElement(inv);
         if (t instanceof CtVariableRead) {
             CtVariableReference<?> v = ((CtVariableRead<?>) t).getVariable();
             String c = v.getType().toString();
@@ -278,7 +282,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv, CtB
             String typeNotParametrized = (i > 0) ? c.substring(0, i) : c;
             String methodInClassName = typeNotParametrized + "." + simpleName;
             RefinedFunction fi = rtc.getContext().getFunction(methodInClassName, typeNotParametrized);
-            Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVER!!
+            Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), logging);// TODO REVER!!
 
             // Substitute _ by the variable that we send
             String newName = String.format(rtc.freshFormat, rtc.getContext().getCounter());
@@ -291,10 +295,12 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv, CtB
                     innerRefs = innerRefs.substituteVariable(rtc.THIS, ovi.get().getName());
             }
 
-            rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv);
-            return new Predicate(newName, inv, rtc.getErrorEmitter()); // Return variable that represents the invocation
+            rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, logging);
+            return new Predicate(newName, logging, rtc.getErrorEmitter());// Return variable that represents the
+                                                                          // invocation
         }
         return new Predicate();
+
     }
 
     /**
@@ -310,7 +316,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv, CtB
      * 
      * @throws ParsingException
      */
-    private <T> Predicate getRefinementUnaryVariableWrite(CtExpression<T> ex, CtUnaryOperator<T> operator,
+    private <T> Predicate getRefinementUnaryVariableWrite(LogElement ex, CtUnaryOperator<T> operator,
             CtVariableWrite<T> w, String name) throws ParsingException {
         String newName = String.format(rtc.instanceFormat, name, rtc.getContext().getCounter());
         CtVariable<T> varDecl = w.getVariable().getDeclaration();
@@ -321,7 +327,7 @@ private <T> Predicate getRefinementUnaryVariableWrite(CtExpression<T> ex, CtUnar
 
         Predicate c = getOperatorFromKind(operator.getKind(), ex).substituteVariable(rtc.WILD_VAR, newName);
 
-        rtc.getContext().addVarToContext(newName, w.getType(), metadada, w);
+        rtc.getContext().addVarToContext(newName, w.getType(), metadada, new LogElement(w));
         return Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), c);
     }
 
@@ -371,7 +377,7 @@ private String getOperatorFromKind(BinaryOperatorKind kind) {
         }
     }
 
-    private Predicate getOperatorFromKind(UnaryOperatorKind kind, CtElement elem) throws ParsingException {
+    private Predicate getOperatorFromKind(UnaryOperatorKind kind, LogElement elem) throws ParsingException {
         String ret = null;
         switch (kind) {
         case POSTINC:
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java
index 1202f303..ac195dad 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java
@@ -4,6 +4,8 @@
 import java.util.List;
 import java.util.Optional;
 import java.util.stream.Collectors;
+
+import liquidjava.logging.LogElement;
 import liquidjava.processor.context.ObjectState;
 import liquidjava.processor.context.RefinedFunction;
 import liquidjava.processor.context.RefinedVariable;
@@ -39,10 +41,12 @@ public static <R> void checkFunctionInSupertypes(CtClass<?> klass, CtMethod<R> m
 
     static void transferRefinements(RefinedFunction superFunction, RefinedFunction function, CtMethod<?> method,
             TypeChecker tc) {
+        List<LogElement> logParams = method.getParameters().stream().map(LogElement::new).collect(Collectors.toList());
+        LogElement logMethod = new LogElement(method);
         HashMap<String, String> super2function = getParametersMap(superFunction, function, tc, method);
-        transferReturnRefinement(superFunction, function, method, tc, super2function);
-        transferArgumentsRefinements(superFunction, function, method, tc, super2function);
-        transferStateRefinements(superFunction, function, method, tc);
+        transferReturnRefinement(superFunction, function, logMethod, tc, super2function);
+        transferArgumentsRefinements(superFunction, function, logMethod, logParams, tc, super2function);
+        transferStateRefinements(superFunction, function, logMethod, logParams, tc);
     }
 
     private static HashMap<String, String> getParametersMap(RefinedFunction superFunction, RefinedFunction function,
@@ -55,7 +59,7 @@ private static HashMap<String, String> getParametersMap(RefinedFunction superFun
             m.put(superArgs.get(i).getName(), newName);
             m.put(fArgs.get(i).getName(), newName);
             RefinedVariable rv = tc.getContext().addVarToContext(newName, superArgs.get(i).getType(), new Predicate(),
-                    method.getParameters().get(i));
+                    new LogElement(method.getParameters().get(i)));
             for (CtTypeReference<?> t : fArgs.get(i).getSuperTypes()) {
                 rv.addSuperType(t);
             }
@@ -63,11 +67,10 @@ private static HashMap<String, String> getParametersMap(RefinedFunction superFun
         return m;
     }
 
-    static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedFunction function,
-            CtMethod<?> method, TypeChecker tc, HashMap<String, String> super2function) {
+    static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedFunction function, LogElement method,
+            List<LogElement> params, TypeChecker tc, HashMap<String, String> super2function) {
         List<Variable> superArgs = superFunction.getArguments();
         List<Variable> args = function.getArguments();
-        List<CtParameter<?>> params = method.getParameters();
         for (int i = 0; i < args.size(); i++) {
             Variable arg = args.get(i);
             Variable superArg = superArgs.get(i);
@@ -79,7 +82,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF
             if (argRef.isBooleanTrue()) {
                 arg.setRefinement(superArgRef.substituteVariable(newName, arg.getName()));
             } else {
-                boolean f = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition());
+                boolean f = tc.checksStateSMT(superArgRef, argRef, params.get(i));
                 if (!f) {
                     // ErrorPrinter.printError(method, argRef, superArgRef);
                     if (!tc.getErrorEmitter().foundError())
@@ -89,7 +92,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF
         }
     }
 
-    static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunction function, CtMethod<?> method,
+    static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunction function, LogElement method,
             TypeChecker tc, HashMap<String, String> super2function) {
         Predicate functionRef = function.getRefinement();
         Predicate superRef = superFunction.getRefinement();
@@ -128,7 +131,7 @@ static Optional<RefinedFunction> functionInInterface(CtClass<?> klass, String si
     }
 
     private static void transferStateRefinements(RefinedFunction superFunction, RefinedFunction subFunction,
-            CtMethod<?> method, TypeChecker tc) {
+            LogElement method, List<LogElement> params, TypeChecker tc) {
         if (superFunction.hasStateChange()) {
             if (!subFunction.hasStateChange()) {
                 for (ObjectState o : superFunction.getAllStates())
@@ -141,7 +144,7 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi
                     ObjectState subState = subStates.get(i);
 
                     String thisName = String.format(tc.freshFormat, tc.getContext().getCounter());
-                    createVariableInContext(thisName, tc, subFunction, superFunction, method.getParameters().get(i));
+                    createVariableInContext(thisName, tc, subFunction, superFunction, params.get(i));
 
                     Predicate superConst = matchVariableNames(tc.THIS, thisName, superState.getFrom());
                     Predicate subConst = matchVariableNames(tc.THIS, thisName, superFunction, subFunction,
@@ -168,7 +171,7 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi
     }
 
     private static void createVariableInContext(String thisName, TypeChecker tc, RefinedFunction subFunction,
-            RefinedFunction superFunction, CtParameter<?> ctParameter) {
+            RefinedFunction superFunction, LogElement ctParameter) {
         RefinedVariable rv = tc.getContext().addVarToContext(thisName,
                 Utils.getType(subFunction.getTargetClass(), tc.getFactory()), new Predicate(), ctParameter);
         rv.addSuperType(Utils.getType(superFunction.getTargetClass(), tc.getFactory())); // TODO: change: this only
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 b64537cd..def81012 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
@@ -6,6 +6,7 @@
 
 import liquidjava.errors.ErrorEmitter;
 import liquidjava.errors.ErrorHandler;
+import liquidjava.logging.LogElement;
 import liquidjava.processor.context.*;
 import liquidjava.processor.refinement_checker.TypeChecker;
 import liquidjava.processor.refinement_checker.TypeCheckingUtils;
@@ -38,11 +39,11 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
                 Map<String, CtExpression> m = a.getAllValues();
                 CtLiteral<String> from = (CtLiteral<String>) m.get("from");
                 if (from != null) {
-                    ErrorHandler.printErrorConstructorFromState(c, from, tc.getErrorEmitter());
+                    ErrorHandler.printErrorConstructorFromState(new LogElement(c), from, tc.getErrorEmitter());
                     return;
                 }
             }
-            setConstructorStates(f, an, tc, c); // f.setState(an, context.getGhosts(), c);
+            setFunctionStates(f, an, tc, new LogElement(c));// f.setState(an, context.getGhosts(), c);
         } else {
             setDefaultState(f, tc);
         }
@@ -67,7 +68,7 @@ private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<?
             String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to"));
             ObjectState state = new ObjectState();
             if (to != null)
-                state.setTo(new Predicate(to, element, tc.getErrorEmitter()));
+                state.setTo(new Predicate(to, new LogElement(element), tc.getErrorEmitter()));
             l.add(state);
         }
         f.setAllStates(l);
@@ -126,7 +127,7 @@ public static void handleMethodState(CtMethod<?> method, RefinedFunction f, Type
             throws ParsingException {
         List<CtAnnotation<? extends Annotation>> an = getStateAnnotation(method);
         if (!an.isEmpty()) {
-            setFunctionStates(f, an, tc, method);
+            setFunctionStates(f, an, tc, new LogElement(method));
         }
         // f.setState(an, context.getGhosts(), method);
 
@@ -143,7 +144,7 @@ public static void handleMethodState(CtMethod<?> method, RefinedFunction f, Type
      * @throws ParsingException
      */
     private static void setFunctionStates(RefinedFunction f, List<CtAnnotation<? extends Annotation>> anns,
-            TypeChecker tc, CtElement element) throws ParsingException {
+            TypeChecker tc, LogElement element) throws ParsingException {
         List<ObjectState> l = new ArrayList<>();
         for (CtAnnotation<? extends Annotation> an : anns) {
             l.add(getStates(an, f, tc, element));
@@ -153,7 +154,7 @@ private static void setFunctionStates(RefinedFunction f, List<CtAnnotation<? ext
 
     @SuppressWarnings({ "rawtypes" })
     private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnotation, RefinedFunction f,
-            TypeChecker tc, CtElement e) throws ParsingException {
+            TypeChecker tc, LogElement e) throws ParsingException {
         Map<String, CtExpression> m = ctAnnotation.getAllValues();
         String from = TypeCheckingUtils.getStringFromAnnotation(m.get("from"));
         String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to"));
@@ -178,8 +179,8 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
         return state;
     }
 
-    private static Predicate createStatePredicate(String value, /* RefinedFunction f */
-            String targetClass, TypeChecker tc, CtElement e, boolean isTo) throws ParsingException {
+    private static Predicate createStatePredicate(String value, /* RefinedFunction f */ String targetClass,
+            TypeChecker tc, LogElement e, boolean isTo) throws ParsingException {
         Predicate p = new Predicate(value, e, tc.getErrorEmitter());
         String t = targetClass; // f.getTargetClass();
         CtTypeReference<?> r = tc.getFactory().Type().createReference(t);
@@ -193,7 +194,7 @@ private static Predicate createStatePredicate(String value, /* RefinedFunction f
         Predicate c1 = isTo ? getMissingStates(t, tc, p) : p;
         Predicate c = c1.substituteVariable(tc.THIS, name);
         c = c.changeOldMentions(nameOld, name, tc.getErrorEmitter());
-        boolean b = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition());
+        boolean b = tc.checksStateSMT(new Predicate(), c.negate(), e);
         if (b && !tc.getErrorEmitter().foundError()) {
             tc.createSameStateError(e, p, t);
         }
@@ -338,17 +339,20 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) {
                 .substituteVariable(parentTargetName, instanceName);
 
         // StateRefinement(from="true", to="n(this)=this#n")
-        // ObjectState stateChange = getStates(ann, rf, tc, transitionMethod);
+        // ObjectState stateChange =
+
+        LogElement codePlace = new LogElement(fw); // used for logging
 
         ObjectState stateChange = new ObjectState();
         try {
-            Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false);
-            Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true);
+            Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, codePlace,
+                    false);
+            Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, codePlace, true);
             stateChange.setFrom(fromPredicate);
             stateChange.setTo(toPredicate);
         } catch (ParsingException e) {
             ErrorHandler
-                    .printCostumeError(fw,
+                    .printCostumeError(codePlace,
                             "ParsingException while constructing assignment update for `" + fw + "` in class `"
                                     + fw.getVariable().getDeclaringType() + "` : " + e.getMessage(),
                             tc.getErrorEmitter());
@@ -360,10 +364,10 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) {
         Predicate expectState = stateChange.getFrom().substituteVariable(tc.THIS, instanceName)
                 .changeOldMentions(vi.getName(), instanceName, tc.getErrorEmitter());
 
-        if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition
+        if (!tc.checksStateSMT(prevState, expectState, codePlace)) {// Invalid field transition
             if (!tc.getErrorEmitter().foundError()) { // No errors in errorEmitter
                 String states = stateChange.getFrom().toString();
-                tc.createStateMismatchError(fw, fw.toString(), prevState, states);
+                tc.createStateMismatchError(codePlace, fw.toString(), prevState, states);
             }
             return;
         }
@@ -376,7 +380,7 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) {
         // update of stata of new instance of this#n#(whatever it was + 1)
 
         VariableInstance vi2 = (VariableInstance) tc.getContext().addInstanceToContext(newInstanceName, vi.getType(),
-                vi.getRefinement(), fw);
+                vi.getRefinement(), codePlace);
         vi2.setRefinement(transitionedState);
 
         RefinedVariable rv = tc.getContext().getVariableByName(parentTargetName);
@@ -435,7 +439,7 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi,
             }
             expectState = expectState.changeOldMentions(vi.getName(), instanceName, tc.getErrorEmitter());
 
-            found = tc.checksStateSMT(prevCheck, expectState, invocation.getPosition());
+            found = tc.checksStateSMT(prevCheck, expectState, new LogElement(invocation));
             if (found && stateChange.hasTo()) {
                 String newInstanceName = String.format(tc.instanceFormat, name, tc.getContext().getCounter());
                 Predicate transitionedState = stateChange.getTo().substituteVariable(tc.WILD_VAR, newInstanceName)
@@ -454,7 +458,7 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi,
                     .map(Predicate::toString).collect(Collectors.joining(","));
 
             String simpleInvocation = invocation.toString(); // .getExecutable().toString();
-            tc.createStateMismatchError(invocation, simpleInvocation, prevState, states);
+            tc.createStateMismatchError(new LogElement(invocation), simpleInvocation, prevState, states);
             // ErrorPrinter.printStateMismatch(invocation, simpleInvocation, prevState,
             // states);
         }
@@ -527,7 +531,7 @@ private static Predicate sameState(TypeChecker tc, VariableInstance variableInst
     private static String addInstanceWithState(TypeChecker tc, String superName, String name2,
             VariableInstance prevInstance, Predicate transitionedState, CtElement invocation) {
         VariableInstance vi2 = (VariableInstance) tc.getContext().addInstanceToContext(name2, prevInstance.getType(),
-                prevInstance.getRefinement(), invocation);
+                prevInstance.getRefinement(), new LogElement(invocation));
         // vi2.setState(transitionedState);
         vi2.setRefinement(transitionedState);
         RefinedVariable rv = tc.getContext().getVariableByName(superName);
@@ -568,7 +572,7 @@ static String searchFistVariableTarget(TypeChecker tc, CtElement target2, CtElem
                 RefinedVariable var = tc.getContext().getVariableByName(name);
                 String nName = String.format(tc.instanceFormat, name, tc.getContext().getCounter());
                 RefinedVariable rv = tc.getContext().addInstanceToContext(nName, var.getType(),
-                        var.getRefinement().substituteVariable(name, nName), target2);
+                        var.getRefinement().substituteVariable(name, nName), new LogElement(target2));
                 tc.getContext().addRefinementInstanceToVariable(name, nName);
                 invocation.putMetadata(tc.TARGET_KEY, rv);
             }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java
index 62284b25..13b21239 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java
@@ -1,22 +1,23 @@
 package liquidjava.rj_language;
 
 import liquidjava.errors.ErrorEmitter;
+import liquidjava.logging.LogElement;
 import liquidjava.rj_language.parsing.ParsingException;
 import spoon.reflect.declaration.CtElement;
 
 public class BuiltinFunctionPredicate extends Predicate {
 
-    public BuiltinFunctionPredicate(ErrorEmitter ee, CtElement elem, String functionName, String... params)
+    public BuiltinFunctionPredicate(ErrorEmitter ee, LogElement elem, String functionName, String... params)
             throws ParsingException {
         super(functionName + "(" + getFormattedParams(params) + ")", elem, ee);
     }
 
-    public static BuiltinFunctionPredicate builtin_length(String param, CtElement elem, ErrorEmitter ee)
+    public static BuiltinFunctionPredicate builtin_length(String param, LogElement elem, ErrorEmitter ee)
             throws ParsingException {
         return new BuiltinFunctionPredicate(ee, elem, "length", param);
     }
 
-    public static BuiltinFunctionPredicate builtin_addToIndex(String array, String index, String value, CtElement elem,
+    public static BuiltinFunctionPredicate builtin_addToIndex(String array, String index, String value, LogElement elem,
             ErrorEmitter ee) throws ParsingException {
         return new BuiltinFunctionPredicate(ee, elem, "addToIndex", index, value);
     }
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 de738fa6..5999b596 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
@@ -7,6 +7,7 @@
 import java.util.stream.Collectors;
 import liquidjava.errors.ErrorEmitter;
 import liquidjava.errors.ErrorHandler;
+import liquidjava.logging.LogElement;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostState;
@@ -50,7 +51,7 @@ public Predicate() {
      * 
      * @throws ParsingException
      */
-    public Predicate(String ref, CtElement element, ErrorEmitter e) throws ParsingException {
+    public Predicate(String ref, LogElement element, ErrorEmitter e) throws ParsingException {
         exp = parse(ref, element, e);
         if (e.foundError())
             return;
@@ -64,7 +65,7 @@ public Predicate(Expression e) {
         exp = e;
     }
 
-    protected Expression parse(String ref, CtElement element, ErrorEmitter e) throws ParsingException {
+    protected Expression parse(String ref, LogElement element, ErrorEmitter e) throws ParsingException {
         try {
             return RefinementsParser.createAST(ref);
         } catch (ParsingException e1) {