From 0fd1c00053aaf67bb622bfa8e4794eceab65bbba Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 6 Feb 2013 09:40:16 -0800
Subject: [PATCH] fix reference counting bug in qe

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz_qe/qe_arith_plugin.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/muz_qe/qe_arith_plugin.cpp b/src/muz_qe/qe_arith_plugin.cpp
index 4e158229b..1baee51fa 100644
--- a/src/muz_qe/qe_arith_plugin.cpp
+++ b/src/muz_qe/qe_arith_plugin.cpp
@@ -524,7 +524,8 @@ namespace qe {
                 expr_ref as_bt_le_0(result, m), tmp2(m), tmp3(m), tmp4(m);
                 
                 // a*s + b*t + (a-1)(b-1) <= 0
-                mk_le(m_arith.mk_add(as_bt, slack), result1);
+                tmp2 = m_arith.mk_add(as_bt, slack);
+                mk_le(tmp2, result1);
                 
                 rational a1 = a, b1 = b;
                 if (abs_a < abs_b) {