mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-09-28 16:42:14 -07:00
parent 476b06fa14 9fa7cd48e9
commit ab3b36269e
5 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_util.py
View file

@ -1482,7 +1482,7 @@ class PythonInstallComponent(Component):
else: else:
MakeRuleCmd.install_files(out, MakeRuleCmd.install_files(out,
os.path.join('python', 'z3', '*.pyc'), os.path.join('python', 'z3', '*.pyc'),
self.pythonPkgDir, os.path.join(self.pythonPkgDir,'z3'),
in_prefix=self.in_prefix_install) in_prefix=self.in_prefix_install)
if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): 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) out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)

2
src/api/python/z3test.py
View file

@ -12,7 +12,7 @@ if len(sys.argv) < 2 or sys.argv[1] == 'z3':
elif sys.argv[1] == 'z3num': elif sys.argv[1] == 'z3num':
r = doctest.testmod(z3.z3num) r = doctest.testmod(z3.z3num)
else: else:
print 'Usage: z3test.py (z3 | z3num)' print('Usage: z3test.py (z3 | z3num)')
sys.exit(1) sys.exit(1)
if r.failed != 0: if r.failed != 0:

3
src/ast/pattern/expr_pattern_match.cpp
View file

@ -388,7 +388,10 @@ expr_pattern_match::initialize(char const * spec_string) {
std::istringstream is(spec_string); std::istringstream is(spec_string);
cmd_context ctx(true, &m_manager); cmd_context ctx(true, &m_manager);
bool ps = ctx.print_success_enabled();
ctx.set_print_success(false);
VERIFY(parse_smt2_commands(ctx, is)); VERIFY(parse_smt2_commands(ctx, is));
ctx.set_print_success(ps);
ptr_vector<expr>::const_iterator it = ctx.begin_assertions(); ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions(); ptr_vector<expr>::const_iterator end = ctx.end_assertions();

8
src/test/mpff.cpp
View file

@ -207,7 +207,7 @@ static void tst_set64(unsigned N, unsigned prec) {
mpff_manager fm(prec); mpff_manager fm(prec);
scoped_mpff a(fm); scoped_mpff a(fm);
fm.set(a, INT64_MAX); fm.set(a, static_cast<int64>(INT64_MAX));
SASSERT(fm.is_int64(a)); SASSERT(fm.is_int64(a));
SASSERT(fm.is_uint64(a)); SASSERT(fm.is_uint64(a));
fm.inc(a); fm.inc(a);
@ -221,7 +221,7 @@ static void tst_set64(unsigned N, unsigned prec) {
SASSERT(fm.is_int64(a)); SASSERT(fm.is_int64(a));
SASSERT(fm.is_uint64(a)); SASSERT(fm.is_uint64(a));
fm.set(a, INT64_MIN); fm.set(a, static_cast<int64>(INT64_MIN));
SASSERT(fm.is_int64(a)); SASSERT(fm.is_int64(a));
SASSERT(!fm.is_uint64(a)); SASSERT(!fm.is_uint64(a));
fm.dec(a); fm.dec(a);
@ -235,7 +235,7 @@ static void tst_set64(unsigned N, unsigned prec) {
SASSERT(fm.is_int64(a)); SASSERT(fm.is_int64(a));
SASSERT(!fm.is_uint64(a)); SASSERT(!fm.is_uint64(a));
fm.set(a, UINT64_MAX); fm.set(a, static_cast<uint64>(UINT64_MAX));
SASSERT(fm.is_uint64(a)); SASSERT(fm.is_uint64(a));
SASSERT(!fm.is_int64(a)); SASSERT(!fm.is_int64(a));
fm.inc(a); fm.inc(a);
@ -600,7 +600,7 @@ static void tst_div(unsigned prec) {
scoped_mpff a(m), b(m), c(m); scoped_mpff a(m), b(m), c(m);
m.round_to_plus_inf(); m.round_to_plus_inf();
m.set(a, 1); m.set(a, 1);
m.set(b, UINT64_MAX); m.set(b, static_cast<uint64>(UINT64_MAX));
m.div(a, b, c); m.div(a, b, c);
m.display_raw(std::cout, a); std::cout << "\n"; m.display_raw(std::cout, a); std::cout << "\n";
m.display_raw(std::cout, b); std::cout << "\n"; m.display_raw(std::cout, b); std::cout << "\n";

2
src/test/mpz.cpp
View file

@ -280,7 +280,7 @@ void tst_int_min_bug() {
mpz big; mpz big;
mpz expected; mpz expected;
mpz r; mpz r;
m.set(big, UINT64_MAX); m.set(big, static_cast<uint64>(UINT64_MAX));
m.set(expected, "18446744075857035263"); m.set(expected, "18446744075857035263");
m.sub(big, intmin, r); m.sub(big, intmin, r);
std::cout << "r: " << m.to_string(r) << "\nexpected: " << m.to_string(expected) << "\n"; std::cout << "r: " << m.to_string(r) << "\nexpected: " << m.to_string(expected) << "\n";