From 78cc1e0703bac20f6cf4eb2f0c1e26992f347afc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 29 Apr 2015 15:15:57 +0100 Subject: [PATCH 1/2] Remove temporary files created during configuration tests. --- scripts/mk_util.py | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 547379aecee..e40a549a167 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -227,7 +227,13 @@ def test_openmp(cc): t.add('#include\nint main() { return omp_in_parallel() ? 1 : 0; }\n') t.commit() if IS_WINDOWS: - return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '/openmp']) == 0 + r = exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '/openmp']) == 0 + try: + rmf('tstomp.obj') + rmf('tstomp.exe') + except: + pass + return r else: return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0 @@ -357,10 +363,14 @@ def check_ml(): r = exec_cmd([OCAMLOPT, '-o', 'a.out', 'hello.ml']) if r != 0: raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.') - rmf('hello.cmi') - rmf('hello.cmo') - rmf('hello.cmx') - rmf('a.out') + try: + rmf('hello.cmi') + rmf('hello.cmo') + rmf('hello.cmx') + rmf('a.out') + rmf('hello.o') + except: + pass find_ml_lib() find_ocaml_find() From 4e082eae6e591bd6cdb745637b2e9c983b2ef073 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 29 Apr 2015 15:16:25 +0100 Subject: [PATCH 2/2] Version number adjustment. --- RELEASE_NOTES | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index afa613f5736..2c7e2e0fbb2 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -1,6 +1,6 @@ RELEASE NOTES -Version 4.4 +Version 4.4.0 ============= - New feature: Support for the theory of floating-point numbers. This comes in the form of logics (QF_FP and QF_FPBV), tactics (qffp and qffpbv), as well as a theory plugin that allows theory combinations. Z3 supports the official SMT theory definition of FP (see http://smtlib.cs.uiowa.edu/theories/FloatingPoint.smt2) in SMT2 files, as well as all APIs.