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 f2274476..88b49687 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java
@@ -17,6 +17,7 @@ public class ContextHistory {
     private Set<GhostState> ghosts;
     private Set<AliasWrapper> aliases;
     private Set<RefinedVariable> globalVars;
+    private Set<RefinedFunction> methods;
 
     private ContextHistory() {
         fileScopes = new HashMap<>();
@@ -24,6 +25,7 @@ private ContextHistory() {
         globalVars = new HashSet<>();
         ghosts = new HashSet<>();
         aliases = new HashSet<>();
+        methods = new HashSet<>();
     }
 
     public static ContextHistory getInstance() {
@@ -38,6 +40,7 @@ public void clearHistory() {
         globalVars.clear();
         ghosts.clear();
         aliases.clear();
+        methods.clear();
     }
 
     public void saveContext(CtElement element, Context context) {
@@ -56,6 +59,7 @@ public void saveContext(CtElement element, Context context) {
         globalVars.addAll(context.getCtxGlobalVars());
         ghosts.addAll(context.getGhostStates());
         aliases.addAll(context.getAliases());
+        methods.addAll(context.getCtxFunctions());
     }
 
     private String getScopePosition(CtElement element) {
@@ -81,6 +85,10 @@ public Set<AliasWrapper> getAliases() {
         return aliases;
     }
 
+    public Set<RefinedFunction> getMethods() {
+        return methods;
+    }
+
     public Map<String, Set<String>> getFileScopes() {
         return fileScopes;
     }
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 09095f35..e5655d5a 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
@@ -379,7 +379,7 @@ public void visitCtIf(CtIf ifElement) {
                 thenRefs = Predicate.createConjunction(expRefs, freshIsTrue);
                 elseRefs = Predicate.createConjunction(expRefs, freshIsFalse);
             }
-            
+
             freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp);
         }
         vcChecker.addPathVariable(freshRV);