From 31e2d823c91309d75e5edfe5f82bf07291c38562 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 7 Nov 2013 01:35:25 -0800
Subject: [PATCH] add cutting plane

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_card.cpp | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_card.cpp b/src/smt/theory_card.cpp
index acead0dce..6f54fdd4f 100644
--- a/src/smt/theory_card.cpp
+++ b/src/smt/theory_card.cpp
@@ -113,6 +113,20 @@ namespace smt {
         m_watch_trail.push_back(bv);
     }
 
+    static unsigned gcd(unsigned a, unsigned b) {
+        if (a == 0) return b;
+        if (b == 0) return a;
+        while (a != b) {
+            if (a < b) {
+                b %= a;
+            }
+            else {
+                a %= b;
+            }
+        }
+        return a;
+    }
+
     void theory_card::add_card(card* c) {
         bool_var abv = c->m_bv;
         arg_t& args = c->m_args;
@@ -141,7 +155,7 @@ namespace smt {
                 g = gcd(g, args[i].second);
             }
             if (g > 1) {
-                unsigned k = c->m_k;
+                int k = c->m_k;
                 if (k >= 0) {
                     c->m_k /= g;
                 }