From b94edf8fe68b6658b2a6a31e8835759525265ed2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Oct 2012 23:26:03 -0700 Subject: [PATCH 1/2] improving compilation options Signed-off-by: Leonardo de Moura --- configure.ac | 1 + scripts/config-release.mk.in | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) 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 From 25837290850c41b7fcc507834ebb69b3693db742 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Oct 2012 23:43:58 -0700 Subject: [PATCH 2/2] fixing some compilation warnings Signed-off-by: Leonardo de Moura --- src/muz_qe/proof_utils.h | 2 +- src/muz_qe/qe_lite.h | 2 +- src/test/dl_smt_relation.cpp | 2 +- src/test/map.cpp | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) 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 str2int; + map str2int; str2int.insert("foo", 35); SASSERT(str2int.contains("foo")); SASSERT(str2int.find_iterator("foo") != str2int.end());