diff --git a/logics/rsltl_encoder.py b/logics/rsltl_encoder.py
index 62da203..79844b8 100644
--- a/logics/rsltl_encoder.py
+++ b/logics/rsltl_encoder.py
@@ -17,6 +17,7 @@ class rsLTL_Encoder(object):
     
     def get_encoding(self, formula, bound):
         self.cache_init(bound)
+        self.init_ncalls()
         return self.encode(formula, 0, bound)
         
     def init_ncalls(self):
@@ -53,7 +54,11 @@ class rsLTL_Encoder(object):
 
     def get_cache_hits(self):
         return self.cache_hits
-        
+    
+    def flush_cache(self):
+        self.enc_fcache = None
+        self.enc_fcache_approx = None
+    
     def get_ncalls(self):
         return (self.ncalls_encode, self.ncalls_encode_approx)
         
diff --git a/smt/smt_checker_rsc.py b/smt/smt_checker_rsc.py
index 413daaf..0aafe79 100644
--- a/smt/smt_checker_rsc.py
+++ b/smt/smt_checker_rsc.py
@@ -408,12 +408,16 @@ class SmtCheckerRSC(object):
 
             # reachability test:
             self.solver.push()
+            
             print("[" + colour_str(C_BOLD, "i") + "] Generating the formula encoding...")
-            encoder.init_ncalls()
+            
             f = encoder.get_encoding(formula, self.current_level)
             ncalls = encoder.get_ncalls()
+            
             print("[" + colour_str(C_BOLD, "i") + "] Cache hits: " + str(encoder.get_cache_hits()) + ", encode calls: " + str(ncalls[0]) + " (approx: " + str(ncalls[1]) + ")")
             print("[" + colour_str(C_BOLD, "i") + "] Adding the formula to the solver...")
+            
+            encoder.flush_cache()
             self.solver.add(f)
             
             print("[" + colour_str(C_BOLD, "i") + "] Adding the loops encoding...")