diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc
index 501393d..b450b73 100644
--- a/minisat/core/Solver.cc
+++ b/minisat/core/Solver.cc
@@ -210,7 +210,7 @@ void Solver::cancelUntil(int level) {
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
             assigns [x] = l_Undef;
-            if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
+            if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
                 polarity[x] = sign(trail[c]);
             insertVarOrder(x); }
         qhead = trail_lim[level];
@@ -666,7 +666,7 @@ lbool Solver::search(int nof_conflicts)
 
         }else{
             // NO CONFLICT
-            if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
+            if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
                 // Reached bound on number of conflicts:
                 progress_estimate = progressEstimate();
                 cancelUntil(0);
diff --git a/minisat/core/SolverTypes.h b/minisat/core/SolverTypes.h
index 4757b20..c3fae2b 100644
--- a/minisat/core/SolverTypes.h
+++ b/minisat/core/SolverTypes.h
@@ -47,7 +47,7 @@ struct Lit {
     int     x;
 
     // Use this as a constructor:
-    friend Lit mkLit(Var var, bool sign = false);
+    //friend Lit mkLit(Var var, bool sign = false);
 
     bool operator == (Lit p) const { return x == p.x; }
     bool operator != (Lit p) const { return x != p.x; }
@@ -55,7 +55,7 @@ struct Lit {
 };
 
 
-inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
+inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
 inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
 inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
 inline  bool sign      (Lit p)              { return p.x & 1; }
@@ -127,7 +127,10 @@ class Clause {
         unsigned has_extra : 1;
         unsigned reloced   : 1;
         unsigned size      : 27; }                        header;
+#include <util/pragma_push.def>
+#include <util/pragma_wzero_length_array.def>
     union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
+#include <util/pragma_pop.def>
 
     friend class ClauseAllocator;
 
@@ -142,11 +145,12 @@ class Clause {
         for (int i = 0; i < ps.size(); i++) 
             data[i].lit = ps[i];
 
-        if (header.has_extra)
+        if (header.has_extra) {
             if (header.learnt)
                 data[header.size].act = 0;
             else
                 calcAbstraction();
+        }
     }
 
     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
@@ -157,11 +161,12 @@ class Clause {
         for (int i = 0; i < from.size(); i++)
             data[i].lit = from[i];
 
-        if (header.has_extra)
+        if (header.has_extra) {
             if (header.learnt)
                 data[header.size].act = from.data[header.size].act;
             else 
                 data[header.size].abs = from.data[header.size].abs;
+        }
     }
 
 public:
diff --git a/minisat/mtl/IntTypes.h b/minisat/mtl/IntTypes.h
index c488162..e8e24bd 100644
--- a/minisat/mtl/IntTypes.h
+++ b/minisat/mtl/IntTypes.h
@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #else
 
 #   include <stdint.h>
+#ifndef _MSC_VER
 #   include <inttypes.h>
+#endif
 
 #endif
 
diff --git a/minisat/mtl/Vec.h b/minisat/mtl/Vec.h
index b225911..d46e169 100644
--- a/minisat/mtl/Vec.h
+++ b/minisat/mtl/Vec.h
@@ -96,7 +96,7 @@ template<class T>
 void vec<T>::capacity(int min_cap) {
     if (cap >= min_cap) return;
     int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1);   // NOTE: grow by approximately 3/2
-    if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
+    if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
         throw OutOfMemoryException();
  }
 
diff --git a/minisat/simp/SimpSolver.cc b/minisat/simp/SimpSolver.cc
index 1d219a3..5ccdb67 100644
--- a/minisat/simp/SimpSolver.cc
+++ b/minisat/simp/SimpSolver.cc
@@ -130,8 +130,6 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
     return result;
 }
 
-
-
 bool SimpSolver::addClause_(vec<Lit>& ps)
 {
 #ifndef NDEBUG
@@ -227,10 +225,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
         if (var(qs[i]) != v){
             for (int j = 0; j < ps.size(); j++)
                 if (var(ps[j]) == var(qs[i]))
+                {
                     if (ps[j] == ~qs[i])
                         return false;
                     else
                         goto next;
+                }
             out_clause.push(qs[i]);
         }
         next:;
@@ -261,10 +261,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
         if (var(__qs[i]) != v){
             for (int j = 0; j < ps.size(); j++)
                 if (var(__ps[j]) == var(__qs[i]))
+                {
                     if (__ps[j] == ~__qs[i])
                         return false;
                     else
                         goto next;
+                }
             size++;
         }
         next:;
diff --git a/minisat/utils/Options.h b/minisat/utils/Options.h
index 2dba10f..7d2e83a 100644
--- a/minisat/utils/Options.h
+++ b/minisat/utils/Options.h
@@ -60,7 +60,7 @@ class Option
     struct OptionLt {
         bool operator()(const Option* x, const Option* y) {
             int test1 = strcmp(x->category, y->category);
-            return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
+            return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
         }
     };
 
@@ -282,15 +282,15 @@ class Int64Option : public Option
         if (range.begin == INT64_MIN)
             fprintf(stderr, "imin");
         else
-            fprintf(stderr, "%4"PRIi64, range.begin);
+            fprintf(stderr, "%4" PRIi64, range.begin);
 
         fprintf(stderr, " .. ");
         if (range.end == INT64_MAX)
             fprintf(stderr, "imax");
         else
-            fprintf(stderr, "%4"PRIi64, range.end);
+            fprintf(stderr, "%4" PRIi64, range.end);
 
-        fprintf(stderr, "] (default: %"PRIi64")\n", value);
+        fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
         if (verbose){
             fprintf(stderr, "\n        %s\n", description);
             fprintf(stderr, "\n");
diff --git a/minisat/utils/Options.cc b/minisat/utils/Options.cc
index 83c40e8..15bfca1 100644
--- a/minisat/utils/Options.cc
+++ b/minisat/utils/Options.cc
@@ -43,10 +43,12 @@ void Minisat::parseOptions(int& argc, char** argv, bool strict)
             }

             if (!parsed_ok)
+            {
                 if (strict && match(argv[i], "-"))
                     fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()), exit(1);
                 else
                     argv[j++] = argv[i];
+            }
         }
     }

diff --git a/minisat/utils/ParseUtils.h b/minisat/utils/ParseUtils.h
index d307164..7b46f09 100644
--- a/minisat/utils/ParseUtils.h
+++ b/minisat/utils/ParseUtils.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <stdlib.h>
 #include <stdio.h>
 
-#include <zlib.h>
+//#include <zlib.h>
 
 namespace Minisat {
 
@@ -35,7 +35,7 @@ static const int buffer_size = 1048576;
 
 
 class StreamBuffer {
-    gzFile        in;
+    //gzFile        in;
     unsigned char buf[buffer_size];
     int           pos;
     int           size;
@@ -43,10 +43,10 @@ class StreamBuffer {
     void assureLookahead() {
         if (pos >= size) {
             pos  = 0;
-            size = gzread(in, buf, sizeof(buf)); } }
+            /*size = gzread(in, buf, sizeof(buf));*/ } }
 
 public:
-    explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
+    //explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
 
     int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }
     void operator ++ ()       { pos++; assureLookahead(); }
diff --git a/minisat/utils/System.h b/minisat/utils/System.h
index 9cbbc51..27b9700 100644
--- a/minisat/utils/System.h
+++ b/minisat/utils/System.h
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_System_h
 #define Minisat_System_h
 
-#if defined(__linux__)
+#if defined(__linux__) && defined(__GLIBC__)
 #include <fpu_control.h>
 #endif
 
diff --git a/minisat/mtl/Vec.h b/minisat/mtl/Vec.h
--- a/minisat/mtl/Vec.h
+++ b/minisat/mtl/Vec.h
@@ -96,8 +96,10 @@
 void vec<T>::capacity(int min_cap) {
     if (cap >= min_cap) return;
     int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1);   // NOTE: grow by approximately 3/2
-    if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
-        throw OutOfMemoryException();
+    if (add > INT_MAX - cap)
+      throw OutOfMemoryException();
+
+    data = (T*)xrealloc(data, (cap += add) * sizeof(T));
  }
 
 
diff --git a/minisat/mtl/XAlloc.h b/minisat/mtl/XAlloc.h
--- a/minisat/mtl/XAlloc.h
+++ b/minisat/mtl/XAlloc.h
@@ -21,7 +21,6 @@
 #ifndef Minisat_XAlloc_h
 #define Minisat_XAlloc_h
 
-#include <errno.h>
 #include <stdlib.h>
 
 namespace Minisat {
@@ -33,7 +32,7 @@
 static inline void* xrealloc(void *ptr, size_t size)
 {
     void* mem = realloc(ptr, size);
-    if (mem == NULL && errno == ENOMEM){
+    if (mem == NULL){
         throw OutOfMemoryException();
     }else
         return mem;