From da01f237fd298deac36b13813bce2308f1995bf5 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sat, 7 Feb 2015 18:06:13 +0000
Subject: [PATCH] fixed memory leaks

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/tactic/arith/propagate_ineqs_tactic.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp
index d7e4f30d2..977f15167 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.cpp
+++ b/src/tactic/arith/propagate_ineqs_tactic.cpp
@@ -115,6 +115,7 @@ struct propagate_ineqs_tactic::imp {
                 out << "< oo";
             out << "\n";
         }
+        nm.del(k);
     }
 
     a_var mk_var(expr * t) {
@@ -234,6 +235,7 @@ struct propagate_ineqs_tactic::imp {
             SASSERT(k == GE);
             bp.assert_lower(x, c_prime, strict);
         }
+        nm.del(c_prime);
         return true;
     }
 
@@ -309,6 +311,8 @@ struct propagate_ineqs_tactic::imp {
                     m_new_goal->assert_expr(m_util.mk_le(p, m_util.mk_numeral(rational(u), m_util.is_int(p))));
             }
         }
+        nm.del(l);
+        nm.del(u);
     }
     
     bool is_x_minus_y_eq_0(expr * t, expr * & x, expr * & y) {