diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp
index e5922fd8c..cf38719a9 100644
--- a/src/sat/smt/q_mam.cpp
+++ b/src/sat/smt/q_mam.cpp
@@ -3333,6 +3333,8 @@ namespace q {
         }
 
         void update_vars(unsigned short var_id, path * p, quantifier * qa, app * mp) {
+            if (var_id >= qa->get_num_decls())
+                return;
             paths & var_paths = m_var_paths[var_id];
             bool found = false;
             for (path* curr_path : var_paths) {