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());