diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 529ed72e8..510d517be 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6485,7 +6485,7 @@ class ModelRef(Z3PPObject): sat >>> m = s.model() >>> m.get_universe(A) - [A!val!0, A!val!1] + [A!val!1, A!val!0] """ if z3_debug(): _z3_assert(isinstance(s, SortRef), "Z3 sort expected") diff --git a/src/math/lp/int_gcd_test.cpp b/src/math/lp/int_gcd_test.cpp index 8891f495f..4801cc436 100644 --- a/src/math/lp/int_gcd_test.cpp +++ b/src/math/lp/int_gcd_test.cpp @@ -259,7 +259,7 @@ namespace lp { bool int_gcd_test::accumulate_parity(const row_strip & row, unsigned least_idx) { // remove this line to enable new functionality. - return true; + // return true; mpq modulus(0); bool least_sign = false;