mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

Wignored-qualifiers

Browse source
This commit is contained in:
Daniel J. Hofmann 2015-04-03 19:24:35 +02:00
parent 4e59ba922b
commit 6150083276
2 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/rel/dl_sparse_table.h
View file

@ -350,7 +350,7 @@ namespace datalog {
*ptr&=m_write_mask; *ptr&=m_write_mask;
*ptr|=val<<m_small_offset; *ptr|=val<<m_small_offset;
} }
unsigned const next_ofs() const { return m_offset+m_length; } unsigned next_ofs() const { return m_offset+m_length; }
}; };
class column_layout : public svector<column_info> { class column_layout : public svector<column_info> {

6
src/util/hwf.h
View file

@ -127,15 +127,15 @@ public:
void to_rational(hwf const & x, scoped_mpq & o) { to_rational(x, o.m(), o); } 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; return (x.get_raw() & 0x8000000000000000ull) != 0;
} }
const uint64 sig(hwf const & x) const { uint64 sig(hwf const & x) const {
return x.get_raw() & 0x000FFFFFFFFFFFFFull; 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; return ((x.get_raw() & 0x7FF0000000000000ull) >> 52) - 1023;
} }