diff -urN glpk-4.65.orig/src/minisat/minisat.c glpk-4.65/src/minisat/minisat.c
--- glpk-4.65.orig/src/minisat/minisat.c	2018-02-16 00:00:00.000000000 -0700
+++ glpk-4.65/src/minisat/minisat.c	2018-05-20 18:54:25.106624859 -0600
@@ -135,11 +135,11 @@ struct clause_t
 
 #define clause_learnt(c) ((c)->size_learnt & 1)
 
-#define clause_activity(c) \
-    (*((float*)&(c)->lits[(c)->size_learnt>>1]))
+#define clause_activity(c, a) \
+    memcpy(&(a), &(c)->lits[(c)->size_learnt>>1], sizeof(float))
 
 #define clause_setactivity(c, a) \
-    (void)(*((float*)&(c)->lits[(c)->size_learnt>>1]) = (a))
+    memcpy(&(c)->lits[(c)->size_learnt>>1], &(a), sizeof(float))
 
 /*====================================================================*/
 /* Encode literals in clause pointers: */
@@ -313,14 +313,18 @@ static inline void act_clause_rescale(so
     clause** cs = (clause**)vecp_begin(&s->learnts);
     int i;
     for (i = 0; i < vecp_size(&s->learnts); i++){
-        float a = clause_activity(cs[i]);
-        clause_setactivity(cs[i], a * (float)1e-20);
+        float a;
+        clause_activity(cs[i], a);
+        a *= (float)1e-20;
+        clause_setactivity(cs[i], a);
     }
     s->cla_inc *= (float)1e-20;
 }
 
 static inline void act_clause_bump(solver* s, clause *c) {
-    float a = clause_activity(c) + s->cla_inc;
+    float a;
+    clause_activity(c, a);
+    a += s->cla_inc;
     clause_setactivity(c,a);
     if (a > 1e20) act_clause_rescale(s);
 }
@@ -356,7 +360,7 @@ static clause* clause_new(solver* s, lit
         c->lits[i] = begin[i];
 
     if (learnt)
-        *((float*)&c->lits[size]) = 0.0;
+        memset(&c->lits[size], 0, sizeof(float));
 
     assert(begin[0] >= 0);
     assert(begin[0] < s->size*2);
@@ -850,10 +854,17 @@ clause* solver_propagate(solver* s)
 }
 
 static inline int clause_cmp (const void* x, const void* y) {
-    return clause_size((clause*)x) > 2
-           && (clause_size((clause*)y) == 2
-               || clause_activity((clause*)x)
-                  < clause_activity((clause*)y)) ? -1 : 1; }
+    clause *cx = (clause *)x;
+    clause *cy = (clause *)y;
+    float fx, fy;
+    if (clause_size(cx) <= 2)
+        return 1;
+    if (clause_size(cy) == 2)
+        return -1;
+    clause_activity(cx, fx);
+    clause_activity(cy, fy);
+    return fx < fy ? -1 : 1;
+}
 
 void solver_reducedb(solver* s)
 {
@@ -874,10 +885,12 @@ void solver_reducedb(solver* s)
             learnts[j++] = learnts[i];
     }
     for (; i < vecp_size(&s->learnts); i++){
+        float f;
+        clause_activity(learnts[i], f);
         if (clause_size(learnts[i]) > 2
             && reasons[lit_var(*clause_begin(learnts[i]))]
                != learnts[i]
-            && clause_activity(learnts[i]) < extra_lim)
+            && f < extra_lim)
             clause_remove(s,learnts[i]);
         else
             learnts[j++] = learnts[i];