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 0655d1f9f99bf52f2fb41ee81d4eb0b0b362865b..38dee2d0b0ca8a2184da8837975a57f72007cbf5 100644 (file)
--- 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 147b101f35ea8fe730b118f1d59723e2b66fb3cc..e7c2b9437e93c6dab73f4c99381f5ad68edf8528 100644 (file)
--- 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)