From 092c52e5b7e8e5f9f2883502b10da9f0bc9c91ad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Sep 2016 18:29:26 -0700 Subject: [PATCH 1/5] fix for package directory. issue #744 Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 57f2c7ad1..309b08297 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1482,7 +1482,7 @@ class PythonInstallComponent(Component): else: MakeRuleCmd.install_files(out, os.path.join('python', 'z3', '*.pyc'), - self.pythonPkgDir, + os.path.join(self.pythonPkgDir,'z3'), in_prefix=self.in_prefix_install) if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR) From b758a7a508775ad0a848ab54349c13c2f9f8c2dc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Sep 2016 19:53:48 -0700 Subject: [PATCH 2/5] disable smt-lib success printing when locally parsing database of common pattern rules. Issue #743 Signed-off-by: Nikolaj Bjorner --- src/ast/pattern/expr_pattern_match.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp index 86cad58f8..e18831650 100644 --- a/src/ast/pattern/expr_pattern_match.cpp +++ b/src/ast/pattern/expr_pattern_match.cpp @@ -388,7 +388,10 @@ expr_pattern_match::initialize(char const * spec_string) { std::istringstream is(spec_string); cmd_context ctx(true, &m_manager); + bool ps = ctx.print_success_enabled(); + ctx.set_print_success(false); VERIFY(parse_smt2_commands(ctx, is)); + ctx.set_print_success(ps); ptr_vector::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions(); From 8cf356224e08c872c6656eb7d2cf2c3422c6a2b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Sep 2016 22:24:43 -0700 Subject: [PATCH 3/5] fix python for 3.x Signed-off-by: Nikolaj Bjorner --- src/api/python/z3test.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3test.py b/src/api/python/z3test.py index 9c544f623..4554657e4 100644 --- a/src/api/python/z3test.py +++ b/src/api/python/z3test.py @@ -12,7 +12,7 @@ if len(sys.argv) < 2 or sys.argv[1] == 'z3': elif sys.argv[1] == 'z3num': r = doctest.testmod(z3.z3num) else: - print 'Usage: z3test.py (z3 | z3num)' + print('Usage: z3test.py (z3 | z3num)') sys.exit(1) if r.failed != 0: From 9c48fbba2e4cde49540fd7662740e05e9b507637 Mon Sep 17 00:00:00 2001 From: Gianfranco Costamagna Date: Mon, 26 Sep 2016 08:05:15 +0200 Subject: [PATCH 4/5] Update mpff.cpp to fix build with clang and new gcc --- src/test/mpff.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index 35afcccf3..44930f2bd 100644 --- a/src/test/mpff.cpp +++ b/src/test/mpff.cpp @@ -207,7 +207,7 @@ static void tst_set64(unsigned N, unsigned prec) { mpff_manager fm(prec); scoped_mpff a(fm); - fm.set(a, INT64_MAX); + fm.set(a, static_cast(INT64_MAX)); SASSERT(fm.is_int64(a)); SASSERT(fm.is_uint64(a)); fm.inc(a); @@ -221,7 +221,7 @@ static void tst_set64(unsigned N, unsigned prec) { SASSERT(fm.is_int64(a)); SASSERT(fm.is_uint64(a)); - fm.set(a, INT64_MIN); + fm.set(a, static_cast(INT64_MIN)); SASSERT(fm.is_int64(a)); SASSERT(!fm.is_uint64(a)); fm.dec(a); @@ -235,7 +235,7 @@ static void tst_set64(unsigned N, unsigned prec) { SASSERT(fm.is_int64(a)); SASSERT(!fm.is_uint64(a)); - fm.set(a, UINT64_MAX); + fm.set(a, static_cast(UINT64_MAX)); SASSERT(fm.is_uint64(a)); SASSERT(!fm.is_int64(a)); fm.inc(a); @@ -600,7 +600,7 @@ static void tst_div(unsigned prec) { scoped_mpff a(m), b(m), c(m); m.round_to_plus_inf(); m.set(a, 1); - m.set(b, UINT64_MAX); + m.set(b, static_cast(UINT64_MAX)); m.div(a, b, c); m.display_raw(std::cout, a); std::cout << "\n"; m.display_raw(std::cout, b); std::cout << "\n"; From 4817b87b7d7727f76ae534c76c10c4828c79816c Mon Sep 17 00:00:00 2001 From: Gianfranco Costamagna Date: Mon, 26 Sep 2016 08:06:38 +0200 Subject: [PATCH 5/5] fix build with new gcc and clang compilers --- src/test/mpz.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/mpz.cpp b/src/test/mpz.cpp index d7944ae95..ee7cf39f1 100644 --- a/src/test/mpz.cpp +++ b/src/test/mpz.cpp @@ -280,7 +280,7 @@ void tst_int_min_bug() { mpz big; mpz expected; mpz r; - m.set(big, UINT64_MAX); + m.set(big, static_cast(UINT64_MAX)); m.set(expected, "18446744075857035263"); m.sub(big, intmin, r); std::cout << "r: " << m.to_string(r) << "\nexpected: " << m.to_string(expected) << "\n";