From 86ad8c348e3a1b43e65d062e8f01472c66e79ab5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Nov 2015 14:32:47 -0800
Subject: [PATCH] fix(library/norm_num): memory leaks

---
 src/library/norm_num.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/library/norm_num.cpp b/src/library/norm_num.cpp
index 2a7618dd1..b5cbb060b 100644
--- a/src/library/norm_num.cpp
+++ b/src/library/norm_num.cpp
@@ -1198,5 +1198,11 @@ void finalize_norm_num() {
     delete g_mul_div;
     delete g_nonzero_div;
     delete g_neg_zero;
+    delete g_lin_ord_ring;
+    delete g_lin_ord_semiring;
+    delete g_field;
+    delete g_nonzero_neg;
+    delete g_subst_div;
+    delete g_nonzero_pos;
 }
 }