diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp
index 6737eda748..3f63940291 100644
--- a/src/library/equations_compiler/equations.cpp
+++ b/src/library/equations_compiler/equations.cpp
@@ -283,6 +283,7 @@ void finalize_equations() {
     delete g_equations_opcode;
     delete g_equations_result;
     delete g_equation;
+    delete g_equation_ignore_if_unused;
     delete g_no_equation;
     delete g_equations_result_name;
     delete g_equations_name;
diff --git a/src/library/tactic/smt/hinst_lemmas.cpp b/src/library/tactic/smt/hinst_lemmas.cpp
index d8b6b526c6..6f261c246c 100644
--- a/src/library/tactic/smt/hinst_lemmas.cpp
+++ b/src/library/tactic/smt/hinst_lemmas.cpp
@@ -798,6 +798,7 @@ void initialize_hinst_lemmas() {
 }
 
 void finalize_hinst_lemmas() {
+    delete g_pattern_hint;
     delete g_no_inst_pattern_attr;
     delete g_hinst_lemma_max_steps;
 }