diff --git a/src/muz/rel/dl_sparse_table.h b/src/muz/rel/dl_sparse_table.h index 0222aa6e2..4768d8862 100644 --- a/src/muz/rel/dl_sparse_table.h +++ b/src/muz/rel/dl_sparse_table.h @@ -350,7 +350,7 @@ namespace datalog { *ptr&=m_write_mask; *ptr|=val< { diff --git a/src/util/hwf.h b/src/util/hwf.h index 9059869a0..be8ad7e0e 100644 --- a/src/util/hwf.h +++ b/src/util/hwf.h @@ -127,15 +127,15 @@ public: void to_rational(hwf const & x, scoped_mpq & o) { to_rational(x, o.m(), o); } - bool sgn(hwf const & x) const { + bool sgn(hwf const & x) const { return (x.get_raw() & 0x8000000000000000ull) != 0; } - const uint64 sig(hwf const & x) const { + uint64 sig(hwf const & x) const { return x.get_raw() & 0x000FFFFFFFFFFFFFull; } - const int exp(hwf const & x) const { + int exp(hwf const & x) const { return ((x.get_raw() & 0x7FF0000000000000ull) >> 52) - 1023; }