diff --git a/src/library/class_instance_resolution.cpp b/src/library/class_instance_resolution.cpp
index ab77e7e31..61b9441ec 100644
--- a/src/library/class_instance_resolution.cpp
+++ b/src/library/class_instance_resolution.cpp
@@ -173,6 +173,9 @@ struct cienv {
     }
 
     void reset_cache_and_ctx() {
+        m_next_local_idx = 0;
+        m_next_uvar_idx  = 0;
+        m_next_mvar_idx  = 0;
         m_ctx = list<expr>();
         m_local_instances.clear();
         reset_cache();