diff --git a/configure.ac b/configure.ac
index 54d8acf27..d1fc84848 100644
--- a/configure.ac
+++ b/configure.ac
@@ -119,6 +119,7 @@ AS_IF([test "$host_os" = "Darwin"], [
   SLIBEXTRAFLAGS="-Wl,--no-whole-archive"
   COMP_VERSIONS=
   STATIC_FLAGS=-static
+  CXXFLAGS+=" -fno-strict-aliasing"
 ], [test "${host_os:0:6}" = "CYGWIN"], [
    PLATFORM=win
    SO_EXT=.dll
diff --git a/scripts/config-release.mk.in b/scripts/config-release.mk.in
index 53a50b9db..74d388fec 100644
--- a/scripts/config-release.mk.in
+++ b/scripts/config-release.mk.in
@@ -1,7 +1,7 @@
 
 
 CXX=@CXX@
-CXXFLAGS=@CPPFLAGS@ @CXXFLAGS@ -c -O3 -fomit-frame-pointer -Wall -fopenmp -msse -msse2 -mfpmath=sse
+CXXFLAGS=@CPPFLAGS@ @CXXFLAGS@ -c -O3 -fomit-frame-pointer -fopenmp -msse -msse2 -mfpmath=sse
 CXX_OUT_FLAG=-o
 OBJ_EXT=.o
 LIB_EXT=.a
diff --git a/src/muz_qe/proof_utils.h b/src/muz_qe/proof_utils.h
index a193f6821..53a38592e 100644
--- a/src/muz_qe/proof_utils.h
+++ b/src/muz_qe/proof_utils.h
@@ -38,4 +38,4 @@ public:
 
 };
 
-#endif _PROOF_UTILS_H_
+#endif
diff --git a/src/muz_qe/qe_lite.h b/src/muz_qe/qe_lite.h
index 1a2f98294..96166d7c3 100644
--- a/src/muz_qe/qe_lite.h
+++ b/src/muz_qe/qe_lite.h
@@ -46,4 +46,4 @@ public:
     void operator()(expr_ref& fml, proof_ref& pr);
 };
 
-#endif __QE_LITE_H__
+#endif 
diff --git a/src/test/dl_smt_relation.cpp b/src/test/dl_smt_relation.cpp
index 0a473a7f9..a809af4ca 100644
--- a/src/test/dl_smt_relation.cpp
+++ b/src/test/dl_smt_relation.cpp
@@ -219,7 +219,7 @@ namespace datalog {
         Z3_fixedpoint_add_rule(ctx, dl, Z3_mk_implies(ctx, Z3_mk_and(ctx, 2, body4), pxy), 0);
 
         Z3_lbool r = Z3_fixedpoint_query(ctx, dl, pxy);
-        if (r != l_undef) {
+        if (r != Z3_L_UNDEF) {
             std::cout << Z3_ast_to_string(ctx, Z3_fixedpoint_get_answer(ctx, dl)) << "\n";
         }
 
diff --git a/src/test/map.cpp b/src/test/map.cpp
index 833da23a8..7e2cc7e70 100644
--- a/src/test/map.cpp
+++ b/src/test/map.cpp
@@ -20,7 +20,7 @@ Revision History:
 #include"str_hashtable.h"
 
 static void tst1() {
-  map<char *, int, str_hash_proc, str_eq_proc> str2int;
+  map<char const *, int, str_hash_proc, str_eq_proc> str2int;
   str2int.insert("foo", 35);
   SASSERT(str2int.contains("foo"));
   SASSERT(str2int.find_iterator("foo") != str2int.end());