From d729e89a7b3d05359ba391f978cb3861c9d382a4 Mon Sep 17 00:00:00 2001
From: Anh-Dung Phan <t-anphan@microsoft.com>
Date: Thu, 14 Nov 2013 12:36:39 -0800
Subject: [PATCH] Fix a minor bug on cardinality solver

---
 src/opt/opt_solver.cpp  | 16 ++++++++--------
 src/opt/opt_solver.h    |  4 ++--
 src/smt/theory_card.cpp |  5 +++--
 3 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 02b01912e..fee4a8663 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -109,9 +109,11 @@ namespace opt {
 
         lbool r = m_context.check(num_assumptions, assumptions);
         if (m_is_dump) {
-            std::stringstream buffer;
-            buffer << "opt_solver" << ++g_checksat_count << ".smt2";
-            to_smt2_benchmark(buffer.str().c_str(), "benchmark", "QF_BV");       
+            std::stringstream file_name;
+            file_name << "opt_solver" << ++g_checksat_count << ".smt2";
+            std::ofstream buffer(file_name.str().c_str());
+            to_smt2_benchmark(buffer, "opt_solver", "QF_BV");
+            buffer.close();
         }
         if (r == l_true && m_objective_enabled) {
             m_objective_values.reset();
@@ -212,9 +214,8 @@ namespace opt {
         return dynamic_cast<opt_solver&>(s);
     }
     
-    void opt_solver::to_smt2_benchmark(char const * file_name, char const * name, char const * logic, 
-                                       char const * status, char const * attributes) {
-        std::ofstream buffer(file_name);
+    void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic, 
+                                       char const * status, char const * attributes) {        
         ast_smt_pp pp(m);
         pp.set_benchmark_name(name);
         pp.set_logic(logic);
@@ -225,8 +226,7 @@ namespace opt {
         for (unsigned i = 0; i < get_num_assertions(); ++i) {
             pp.add_assumption(to_expr(get_assertion(i)));
         }
-        pp.display_smt2(buffer, to_expr(m.mk_true()));
-        buffer.close();
+        pp.display_smt2(buffer, to_expr(m.mk_true()));        
     }
 
     opt_solver::toggle_objective::toggle_objective(opt_solver& s, bool new_value): s(s), m_old_value(s.m_objective_enabled) {
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 90ebe3251..de7ef0b1d 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -90,8 +90,8 @@ namespace opt {
         
         smt::theory_opt& get_optimizer();
 
-        void to_smt2_benchmark(char const * file_name, char const * name = "benchmarks", 
-                           char const * logic = "", char const * status = "unknown", char const * attributes = "");
+        void to_smt2_benchmark(std::ofstream & buffer, char const * name = "benchmarks", 
+                               char const * logic = "", char const * status = "unknown", char const * attributes = "");
     };
 }
 
diff --git a/src/smt/theory_card.cpp b/src/smt/theory_card.cpp
index c32b600c1..3aa72baef 100644
--- a/src/smt/theory_card.cpp
+++ b/src/smt/theory_card.cpp
@@ -133,9 +133,10 @@ namespace smt {
     }
 
     static unsigned gcd(unsigned a, unsigned b) {
-        if (a == 0) return b;
-        if (b == 0) return a;
         while (a != b) {
+            if (a == 0) return b;
+            if (b == 0) return a;
+            SASSERT(a != 0 && b != 0);
             if (a < b) {
                 b %= a;
             }