From afd83f41b800e7aef366f154e976dc59adf893d4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 3 Apr 2013 17:03:07 -0700
Subject: [PATCH] fix compiler warnings and errors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz_qe/fdd.h           | 10 +++++++---
 src/test/hilbert_basis.cpp |  2 ++
 src/test/karr.cpp          |  3 ++-
 3 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/muz_qe/fdd.h b/src/muz_qe/fdd.h
index e6808375c..59d5a78f5 100644
--- a/src/muz_qe/fdd.h
+++ b/src/muz_qe/fdd.h
@@ -39,7 +39,7 @@ namespace fdd {
         unsigned   m_ref_count;
         void reset();
     public:
-	node() : m_var(0), m_hi(0), m_lo(0), m_ref_count(0) {}
+        node() : m_var(0), m_lo(0), m_hi(0), m_ref_count(0) {}
         node(unsigned var, node_id l, node_id h): m_var(var), m_lo(l), m_hi(h), m_ref_count(0) {}
 
         unsigned get_hash() const;        
@@ -93,9 +93,13 @@ namespace fdd {
     class manager {
     public:
         typedef int64 Key;
+        typedef node::hash node_hash;
+        typedef node::eq node_eq;
+        typedef config::hash config_hash;
+        typedef config::eq config_eq;
     private:
-        typedef map<node, unsigned, typename node::hash, typename node::eq>   node_table;
-        typedef map<config, node_id, typename config::hash, typename config::eq> insert_cache;
+        typedef map<node, unsigned, node_hash, node_eq>      node_table;
+        typedef map<config, node_id, config_hash, config_eq> insert_cache;
         node_table             m_table;
         insert_cache           m_insert_cache;
         svector<node>          m_nodes;
diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp
index e0a4a8370..4752dd78d 100644
--- a/src/test/hilbert_basis.cpp
+++ b/src/test/hilbert_basis.cpp
@@ -220,6 +220,7 @@ static void on_ctrl_c(int) {
     raise(SIGINT);
 }
 
+#if 0
 static void validate_sat(hilbert_basis& hb) {
     ast_manager m;
     reg_decl_plugins(m);
@@ -239,6 +240,7 @@ static void validate_sat(hilbert_basis& hb) {
     lbool r = sol->check_sat(0,0);
     std::cout << r << "\n";
 }
+#endif
 
 static void saturate_basis(hilbert_basis& hb) {
     signal(SIGINT, on_ctrl_c);
diff --git a/src/test/karr.cpp b/src/test/karr.cpp
index 8770eac94..87debf662 100644
--- a/src/test/karr.cpp
+++ b/src/test/karr.cpp
@@ -54,7 +54,6 @@ namespace karr {
         SASSERT(is_sat == l_true);
         dst.reset();
         unsigned basis_size = hb.get_basis_size();
-        bool first_initial = true;
         for (unsigned i = 0; i < basis_size; ++i) {
             bool is_initial;
             vector<rational> soln;
@@ -165,6 +164,7 @@ namespace karr {
         return v;
     }
 
+#if 0
     static vector<rational> V(int i, int j, int k, int l, int m) {
         vector<rational> v;
         v.push_back(rational(i));
@@ -174,6 +174,7 @@ namespace karr {
         v.push_back(rational(m));
         return v;
     }
+#endif
 
     static vector<rational> V(int i, int j, int k, int l, int x, int y, int z) {
         vector<rational> v;