From: petercol <petercol@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 11 Jan 2012 17:03:00 +0000 (+0000)
Subject: Fix Clang compilation.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=357599fa0d8c20513e25dd5b6983254f734b799a;p=francis%2Fstp.git

Fix Clang compilation.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1501 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/sat/mtl/Map.h b/src/sat/mtl/Map.h
index 0655d1f..38dee2d 100644
--- a/src/sat/mtl/Map.h
+++ b/src/sat/mtl/Map.h
@@ -29,17 +29,17 @@ namespace Minisat {
 // Default hash/equals functions
 //
 
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
 template<class K> struct Hash  { uint32_t operator()(const K& k)               const { return hash(k);  } };
 template<class K> struct Equal { bool     operator()(const K& k1, const K& k2) const { return k1 == k2; } };
 
 template<class K> struct DeepHash  { uint32_t operator()(const K* k)               const { return hash(*k);  } };
 template<class K> struct DeepEqual { bool     operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
 
-static inline uint32_t hash(uint32_t x){ return x; }
-static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
-static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
-static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
-
 
 //=================================================================================================
 // Some primes
diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 147b101..e7c2b94 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1458,26 +1458,26 @@ namespace BEEV
         }
 
       // We store them into here before sorting them.
-      vector<BBNode> t_products[bitWidth];
+      vector<vector<BBNode> > t_products(bitWidth);
 
       for (int i = 0; i < bitWidth; i++)
         {
         if (x[i] != BBTrue && x[i] != BBFalse)
           {
-          pushP(t_products, i, y, x[i], nf);
+          pushP(&t_products[0], i, y, x[i], nf);
           }
 
         // A bit can not be true or false, as well as one of these two.
         if (xt[i] == MINUS_ONE_MT)
           {
-          pushP(t_products, i, notY, BBTrue, nf);
+          pushP(&t_products[0], i, notY, BBTrue, nf);
           t_products[i].push_back(BBTrue);
           booth_recoded.insert(n);
           }
 
         else if (xt[i] == ONE_MT)
           {
-          pushP(t_products, i, y, BBTrue, nf);
+          pushP(&t_products[0], i, y, BBTrue, nf);
           }
 
         if (t_products[i].size() == 0)