diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 205b8f948..875cf449f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1617,8 +1617,11 @@ PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRI 'def_module_params' : def_module_params } def _execfile(file, globals=globals(), locals=locals()): - with open(file, "r") as fh: - exec(fh.read()+"\n", globals, locals) + if sys.version < "2.7": + execfile(file, globals, locals) + else: + with open(file, "r") as fh: + exec(fh.read()+"\n", globals, locals) # Execute python auxiliary scripts that generate extra code for Z3. def exec_pyg_scripts(): diff --git a/src/math/realclosure/mpz_matrix.cpp b/src/math/realclosure/mpz_matrix.cpp index ba89dfb36..799a5817e 100644 --- a/src/math/realclosure/mpz_matrix.cpp +++ b/src/math/realclosure/mpz_matrix.cpp @@ -75,14 +75,14 @@ void mpz_matrix_manager::set(mpz_matrix & A, mpz_matrix const & B) { } void mpz_matrix_manager::tensor_product(mpz_matrix const & A, mpz_matrix const & B, mpz_matrix & C) { - scoped_mpz_matrix _C(*this); - mk(A.m * B.m, A.n * B.n, _C); - for (unsigned i = 0; i < _C.m(); i++) - for (unsigned j = 0; j < _C.n(); j++) + scoped_mpz_matrix CC(*this); + mk(A.m * B.m, A.n * B.n, CC); + for (unsigned i = 0; i < CC.m(); i++) + for (unsigned j = 0; j < CC.n(); j++) nm().mul(A(i / B.m, j / B.n), B(i % B.m, j % B.n), - _C(i, j)); - C.swap(_C); + CC(i, j)); + C.swap(CC); } void mpz_matrix_manager::swap_rows(mpz_matrix & A, unsigned i, unsigned j) {