mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-09 06:44:53 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Nuno Lopes 2026-02-15 16:27:51 +00:00
parent e9556c498b
commit 92158ac607
2 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/util/mpq.h
View file

@ -679,11 +679,11 @@ public:
reset_denominator(a);
}
void set(mpq & a, int n, int d) {
void set(mpq & a, int64_t n, int64_t d) {
SASSERT(d != 0);
if (d < 0) {
SASSERT(d != INT_MIN);
SASSERT(n != INT_MIN);
SASSERT(d != std::numeric_limits<int64_t>());
SASSERT(n != std::numeric_limits<int64_t>());
n = -n;
d = -d;
}

14
src/util/rational.h
View file

@ -50,7 +50,7 @@ public:
explicit rational(uint64_t n) { m().set(m_val, n); }
rational(int n, int d) { m().set(m_val, n, d); }
rational(int64_t n, int64_t d) { m().set(m_val, n, d); }
rational(mpq const & q) { m().set(m_val, q); }
rational(mpq && q) noexcept : m_val(std::move(q)) {}
rational(mpz const & z) { m().set(m_val, z); }
@ -290,7 +290,7 @@ public:
rational r = mod(a,b);
SASSERT(r.is_nonneg());
rational r2 = r;
r2 *= rational(2);
r2 *= rational(2ull);
if (operator<(b, r2)) {
r -= b;
}
@ -510,11 +510,11 @@ public:
}
unsigned get_num_bits() const {
return get_num_digits(rational(2));
return get_num_digits(rational(2ull));
}
unsigned get_num_decimal() const {
return get_num_digits(rational(10));
return get_num_digits(rational(10ull));
}
/**
@ -646,14 +646,14 @@ inline rational operator*(rational const & r1, rational const & r2) {
inline rational operator*(rational const & r1, bool r2) {
UNREACHABLE();
return r1 * rational(r2);
return r1 * rational((uint64_t)r2);
}
inline rational operator*(rational const & r1, int64_t r2) {
return r1 * rational(r2);
}
inline rational operator*(bool r1, rational const & r2) {
inline rational operator*(bool r1, rational const & r2) {
UNREACHABLE();
return rational(r1) * r2;
return rational((uint64_t)r1) * r2;
}
inline rational operator*(int64_t r1, rational const & r2) {