diff --git a/src/util/mpq.h b/src/util/mpq.h index ac96b8b7c1e..db38d87b77c 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -521,7 +521,7 @@ class mpq_manager : public mpz_manager { static unsigned hash(mpz const & a) { return mpz_manager::hash(a); } - static unsigned hash(mpq const & a) { return hash(a.m_num); } + static unsigned hash(mpq const & a) { return hash(a.m_num) + 3*hash(a.m_den); } bool eq(mpz const & a, mpz const & b) { return mpz_manager::eq(a, b); }