diff --git a/scripts/glucose-syrup-patch b/scripts/glucose-syrup-patch
index 138e4a50315..22b34562b8e 100644
--- a/scripts/glucose-syrup-patch
+++ b/scripts/glucose-syrup-patch
@@ -1,6 +1,6 @@
-diff -rupN glucose-syrup/core/Solver.cc glucose-syrup-patched/core/Solver.cc
---- glucose-syrup/core/Solver.cc	2014-10-03 10:10:21.000000000 +0100
-+++ glucose-syrup-patched/core/Solver.cc	2016-07-08 13:06:02.772186004 +0100
+diff -rupNw glucose-syrup/core/Solver.cc glucose-syrup-patched/core/Solver.cc
+--- glucose-syrup/core/Solver.cc	2014-10-03 11:10:21.000000000 +0200
++++ glucose-syrup-patched/core/Solver.cc	2018-04-21 16:58:22.950005391 +0200
 @@ -931,7 +931,6 @@ void Solver::uncheckedEnqueue(Lit p, CRe
  CRef Solver::propagate() {
      CRef confl = CRef_Undef;
@@ -19,9 +19,9 @@ diff -rupN glucose-syrup/core/Solver.cc glucose-syrup-patched/core/Solver.cc
                      // Model found:
                      return l_True;
                  }
-diff -rupN glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTypes.h
---- glucose-syrup/core/SolverTypes.h	2014-10-03 10:10:22.000000000 +0100
-+++ glucose-syrup-patched/core/SolverTypes.h	2016-07-08 13:06:02.772186004 +0100
+diff -rupNw glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTypes.h
+--- glucose-syrup/core/SolverTypes.h	2014-10-03 11:10:22.000000000 +0200
++++ glucose-syrup-patched/core/SolverTypes.h	2018-04-21 16:58:22.950005391 +0200
 @@ -53,7 +53,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
  
  #include <assert.h>
@@ -32,9 +32,20 @@ diff -rupN glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTyp
  
  #include "mtl/IntTypes.h"
  #include "mtl/Alg.h"
-diff -rupN glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h
---- glucose-syrup/mtl/IntTypes.h	2014-10-03 10:10:22.000000000 +0100
-+++ glucose-syrup-patched/mtl/IntTypes.h	2016-07-08 13:06:02.772186004 +0100
+@@ -170,7 +172,10 @@ class Clause {
+       unsigned lbd : BITS_LBD;
+     }  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;
+ 
+diff -rupNw glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h
+--- glucose-syrup/mtl/IntTypes.h	2014-10-03 11:10:22.000000000 +0200
++++ glucose-syrup-patched/mtl/IntTypes.h	2018-04-21 16:58:22.950005391 +0200
 @@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
  #else
  
@@ -45,10 +56,49 @@ diff -rupN glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h
  
  #endif
  
-diff -rupN glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolver.cc
---- glucose-syrup/simp/SimpSolver.cc	2014-10-03 10:10:22.000000000 +0100
-+++ glucose-syrup-patched/simp/SimpSolver.cc	2016-07-08 13:07:00.396187548 +0100
-@@ -687,11 +687,11 @@ bool SimpSolver::eliminate(bool turn_off
+diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h
+--- glucose-syrup/mtl/Vec.h	2014-10-03 11:10:22.000000000 +0200
++++ glucose-syrup-patched/mtl/Vec.h	2018-04-21 16:58:22.950005391 +0200
+@@ -103,7 +103,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 -rupNw glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolver.cc
+--- glucose-syrup/simp/SimpSolver.cc	2014-10-03 11:10:22.000000000 +0200
++++ glucose-syrup-patched/simp/SimpSolver.cc	2018-04-21 16:58:22.950005391 +0200
+@@ -319,10 +319,13 @@ bool SimpSolver::merge(const Clause& _ps
+         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:;
+@@ -353,10 +356,12 @@ bool SimpSolver::merge(const Clause& _ps
+         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:;
+@@ -687,11 +692,11 @@ bool SimpSolver::eliminate(bool turn_off
      //
  
      int toPerform = clauses.size()<=4800000;
@@ -62,7 +112,7 @@ diff -rupN glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolve
      while (toPerform && (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)){
  
          gatherTouchedClauses();
-@@ -760,10 +760,11 @@ bool SimpSolver::eliminate(bool turn_off
+@@ -760,10 +765,11 @@ bool SimpSolver::eliminate(bool turn_off
          checkGarbage();
      }
  
@@ -75,9 +125,21 @@ diff -rupN glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolve
                 
      return ok;
  
-diff -rupN glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUtils.h
---- glucose-syrup/utils/ParseUtils.h	2014-10-03 10:10:22.000000000 +0100
-+++ glucose-syrup-patched/utils/ParseUtils.h	2016-07-08 13:06:02.772186004 +0100
+diff -rupNw glucose-syrup/utils/Options.h glucose-syrup-patched/utils/Options.h
+--- glucose-syrup/utils/Options.h	2014-10-03 11:10:22.000000000 +0200
++++ glucose-syrup-patched/utils/Options.h	2018-04-21 16:58:22.950005391 +0200
+@@ -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);
+         }
+     };
+ 
+diff -rupNw glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUtils.h
+--- glucose-syrup/utils/ParseUtils.h	2014-10-03 11:10:22.000000000 +0200
++++ glucose-syrup-patched/utils/ParseUtils.h	2018-04-21 16:58:22.950005391 +0200
 @@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
  #include <stdio.h>
  #include <math.h>
@@ -109,9 +171,9 @@ diff -rupN glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUti
  
      int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }
      void operator ++ ()       { pos++; assureLookahead(); }
-diff -rupN glucose-syrup/utils/System.h glucose-syrup-patched/utils/System.h
---- glucose-syrup/utils/System.h	2014-10-03 10:10:22.000000000 +0100
-+++ glucose-syrup-patched/utils/System.h	2016-07-08 13:06:02.776186005 +0100
+diff -rupNw glucose-syrup/utils/System.h glucose-syrup-patched/utils/System.h
+--- glucose-syrup/utils/System.h	2014-10-03 11:10:22.000000000 +0200
++++ glucose-syrup-patched/utils/System.h	2018-04-21 16:58:22.950005391 +0200
 @@ -60,8 +60,11 @@ static inline double Glucose::cpuTime(vo
  
  // Laurent: I know that this will not compile directly under Windows... sorry for that
diff --git a/scripts/glucose_CMakeLists.txt b/scripts/glucose_CMakeLists.txt
index 94165238d8a..38506152963 100644
--- a/scripts/glucose_CMakeLists.txt
+++ b/scripts/glucose_CMakeLists.txt
@@ -18,3 +18,5 @@ target_include_directories(glucose-condensed
     PUBLIC
     ${CMAKE_CURRENT_SOURCE_DIR}
 )
+
+target_link_libraries(glucose-condensed util)