diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp
index cc063be951..334487bf20 100644
--- a/src/ast/euf/ho_matcher.cpp
+++ b/src/ast/euf/ho_matcher.cpp
@@ -128,7 +128,7 @@ namespace euf {
             drain_backtrack(ho_matcher &m) : m(m) {}
             ~drain_backtrack() {
                 while (!m.m_backtrack.empty()) {
-                    m.m_backtrack.pop();
+                    m.backtrack();
                 }
             }
         };