Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

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

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

src/muz_qe/proof_utils.h

@@ -38,4 +38,4 @@ public:
 
 };
 
-#endif _PROOF_UTILS_H_
+#endif

src/muz_qe/qe_lite.h

@@ -46,4 +46,4 @@ public:
     void operator()(expr_ref& fml, proof_ref& pr);
 };
 
-#endif __QE_LITE_H__
+#endif 

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";
         }
 

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