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