diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp
index a7feada42..6b9826af7 100644
--- a/src/api/api_rcf.cpp
+++ b/src/api/api_rcf.cpp
@@ -25,24 +25,24 @@ Notes:
 #include"api_context.h"
 #include"realclosure.h"
 
+static rcmanager & rcfm(Z3_context c) {
+    return mk_c(c)->rcfm();
+}
+
+static void reset_rcf_cancel(Z3_context c) {
+    rcfm(c).reset_cancel();
+}
+
+static Z3_rcf_num from_rcnumeral(rcnumeral a) { 
+    return reinterpret_cast<Z3_rcf_num>(a.c_ptr()); 
+}
+
+static rcnumeral to_rcnumeral(Z3_rcf_num a) { 
+    return rcnumeral::mk(a); 
+}
+
 extern "C" {
 
-    static rcmanager & rcfm(Z3_context c) {
-        return mk_c(c)->rcfm();
-    }
-
-    static void reset_rcf_cancel(Z3_context c) {
-        rcfm(c).reset_cancel();
-    }
-
-    static rcnumeral to_rcnumeral(Z3_rcf_num a) { 
-        return rcnumeral::mk(a); 
-    }
-
-    static Z3_rcf_num from_rcnumeral(rcnumeral a) { 
-        return reinterpret_cast<Z3_rcf_num>(a.c_ptr()); 
-    }
-
     void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a) {
         Z3_TRY;
         LOG_Z3_rcf_del(c, a);
diff --git a/src/math/realclosure/mpz_matrix.cpp b/src/math/realclosure/mpz_matrix.cpp
index 836ac35c2..ba89dfb36 100644
--- a/src/math/realclosure/mpz_matrix.cpp
+++ b/src/math/realclosure/mpz_matrix.cpp
@@ -44,7 +44,8 @@ void mpz_matrix_manager::mk(unsigned m, unsigned n, mpz_matrix & A) {
     del(A);
     A.m = m;
     A.n = n;
-    A.a_ij = new (m_allocator) mpz[m*n];
+    void * mem = m_allocator.allocate(sizeof(mpz)*m*n);
+    A.a_ij = new (mem) mpz[m*n];
 }
 
 void mpz_matrix_manager::del(mpz_matrix & A) {
@@ -409,7 +410,7 @@ void mpz_matrix_manager::display(std::ostream & out, mpz_matrix const & A, unsig
                 out << " ";
             std::string s = nm().to_string(A(i, j));
             if (s.size() < cell_width) {
-                unsigned space = cell_width - s.size();
+                unsigned space = cell_width - static_cast<unsigned>(s.size());
                 for (unsigned k = 0; k < space; k++) 
                     out << " ";
             }
diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp
index 09e722f23..394a7102a 100644
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@@ -97,10 +97,10 @@ namespace realclosure {
             void set_upper_is_open(bool f) { m_upper_open = f; }
             numeral const & lower() const { return m_lower; }
             numeral const & upper() const { return m_upper; }
-            bool lower_is_inf() const { return m_lower_inf; }
-            bool upper_is_inf() const { return m_upper_inf; }
-            bool lower_is_open() const { return m_lower_open; }
-            bool upper_is_open() const { return m_upper_open; }
+            bool lower_is_inf() const { return m_lower_inf != 0; }
+            bool upper_is_inf() const { return m_upper_inf != 0; }
+            bool lower_is_open() const { return m_lower_open != 0; }
+            bool upper_is_open() const { return m_upper_open != 0; }
         };
 
         void set_rounding(bool to_plus_inf) { m_manager.m_to_plus_inf = to_plus_inf; }
@@ -112,10 +112,10 @@ namespace realclosure {
         numeral const & upper(interval const & a) const { return a.m_upper; }
         numeral & lower(interval & a) { return a.m_lower; }
         numeral & upper(interval & a) { return a.m_upper; }
-        bool lower_is_open(interval const & a) const { return a.m_lower_open; }
-        bool upper_is_open(interval const & a) const { return a.m_upper_open; }
-        bool lower_is_inf(interval const & a) const { return a.m_lower_inf; }
-        bool upper_is_inf(interval const & a) const { return a.m_upper_inf; }
+        bool lower_is_open(interval const & a) const { return a.lower_is_open(); }
+        bool upper_is_open(interval const & a) const { return a.upper_is_open(); }
+        bool lower_is_inf(interval const & a) const { return a.lower_is_inf(); }
+        bool upper_is_inf(interval const & a) const { return a.upper_is_inf(); }
         
         // Setters
         void set_lower(interval & a, numeral const & n) { m_manager.set(a.m_lower, n); }
@@ -637,7 +637,8 @@ namespace realclosure {
                 return; // interval was already saved.
             to_restore.push_back(v);
             inc_ref(v);
-            v->m_old_interval = new (allocator()) mpbqi();
+	    void * mem = allocator().allocate(sizeof(mpbqi));
+            v->m_old_interval = new (mem) mpbqi();
             set_interval(*(v->m_old_interval), v->m_interval);
         }
         void save_interval(value * v) {
@@ -1201,7 +1202,8 @@ namespace realclosure {
         }
 
         sign_condition * mk_sign_condition(unsigned qidx, int sign, sign_condition * prev_sc) {
-            return new (allocator()) sign_condition(qidx, sign, prev_sc);
+	    void * mem = allocator().allocate(sizeof(sign_condition));
+            return new (mem) sign_condition(qidx, sign, prev_sc);
         }
 
         /**
@@ -1748,7 +1750,8 @@ namespace realclosure {
            M and scs will be empty after this operation.
         */
         sign_det * mk_sign_det(mpz_matrix & M_s, scoped_polynomial_seq const & prs, int_buffer const & taqrs, scoped_polynomial_seq const & qs, scoped_sign_conditions & scs) {
-            sign_det * r = new (allocator()) sign_det();
+	    void * mem = allocator().allocate(sizeof(sign_det));
+            sign_det * r = new (mem) sign_det();
             r->M_s.swap(M_s);
             set_array_p(r->m_prs, prs);
             r->m_taqrs.set(allocator(), taqrs.size(), taqrs.c_ptr());
@@ -1763,7 +1766,8 @@ namespace realclosure {
          */
         algebraic * mk_algebraic(unsigned p_sz, value * const * p, mpbqi const & interval, sign_det * sd, unsigned sc_idx) {
             unsigned idx = next_algebraic_idx();
-            algebraic * r = new (allocator()) algebraic(idx);
+	    void * mem = allocator().allocate(sizeof(algebraic));
+            algebraic * r = new (mem) algebraic(idx);
             m_extensions[extension::ALGEBRAIC].push_back(r);
             
             set_p(r->m_p, p_sz, p);
@@ -2495,7 +2499,8 @@ namespace realclosure {
         }
 
         rational_value * mk_rational() {
-            return new (allocator()) rational_value();
+	    void * mem = allocator().allocate(sizeof(rational_value));
+            return new (mem) rational_value();
         }
 
         /**
diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h
index 1e0ac4ba5..146299b56 100644
--- a/src/math/realclosure/realclosure.h
+++ b/src/math/realclosure/realclosure.h
@@ -267,10 +267,10 @@ namespace realclosure {
         void clean_denominators(numeral const & a, numeral & p, numeral & q);
     };
 
-    class value;
+    struct value;
     class num {
         friend class manager;
-        friend class manager::imp;
+        friend struct manager::imp;
         value * m_value;
     public:
         num():m_value(0) {}
diff --git a/src/util/array.h b/src/util/array.h
index c2358d1a4..a3658c354 100644
--- a/src/util/array.h
+++ b/src/util/array.h
@@ -40,7 +40,7 @@ private:
 
     array & operator=(array const & source);
 
-    void set_data(void * mem, size_t sz) {
+    void set_data(void * mem, unsigned sz) {
         size_t * _mem = static_cast<size_t*>(mem);
         *_mem = sz; 
         _mem ++;
@@ -48,7 +48,7 @@ private:
     }
 
     template<typename Allocator>
-    void allocate(Allocator & a, size_t sz) {
+    void allocate(Allocator & a, unsigned sz) {
         size_t * mem  = reinterpret_cast<size_t*>(a.allocate(space(sz)));
         set_data(mem, sz);
     }
@@ -80,13 +80,13 @@ public:
        \brief Store the array in the given chunk of memory (mem).
        This chunck should be big enough to store space(sz) bytes.
     */
-    array(void * mem, size_t sz, T const * vs) {
+    array(void * mem, unsigned sz, T const * vs) {
         DEBUG_CODE(m_data = 0;);
         set(mem, sz, vs);
     }
 
     // WARNING: the memory allocated will not be automatically freed.
-    array(void * mem, size_t sz, bool init_mem) {
+    array(void * mem, unsigned sz, bool init_mem) {
         DEBUG_CODE(m_data = 0;);
         set_data(mem, sz);
         if (init_mem)
@@ -95,14 +95,14 @@ public:
 
     // WARNING: the memory allocated will not be automatically freed.
     template<typename Allocator>
-    array(Allocator & a, size_t sz, T const * vs) {
+    array(Allocator & a, unsigned sz, T const * vs) {
         DEBUG_CODE(m_data = 0;);
         set(a, sz, vs);
     }
 
     // WARNING: the memory allocated will not be automatically freed.
     template<typename Allocator>
-    array(Allocator & a, size_t sz, bool init_mem) {
+    array(Allocator & a, unsigned sz, bool init_mem) {
         DEBUG_CODE(m_data = 0;);
         allocate(a, sz);
         if (init_mem)
@@ -127,41 +127,41 @@ public:
         }
     }
 
-    void set(void * mem, size_t sz, T const * vs) {
+    void set(void * mem, unsigned sz, T const * vs) {
         SASSERT(m_data == 0);
         set_data(mem, sz);
         init(vs);
     }
     
     template<typename Allocator>
-    void set(Allocator & a, size_t sz, T const * vs) {
+    void set(Allocator & a, unsigned sz, T const * vs) {
         SASSERT(m_data == 0);
         allocate(a, sz);
         init(vs);
     }
 
     template<typename Allocator>
-    void set(Allocator & a, size_t sz, T const & v = T()) {
+    void set(Allocator & a, unsigned sz, T const & v = T()) {
         SASSERT(m_data == 0);
         allocate(a, sz);
         init(v);
     }
 
-    size_t size() const { 
+    unsigned size() const { 
         if (m_data == 0) {
             return 0;  
         }
-        return reinterpret_cast<size_t *>(m_data)[SIZE_IDX]; 
+        return static_cast<unsigned>(reinterpret_cast<size_t *>(m_data)[SIZE_IDX]); 
     }
     
     bool empty() const { return m_data == 0; }
 
-    T & operator[](size_t idx) { 
+    T & operator[](unsigned idx) { 
         SASSERT(idx < size()); 
         return m_data[idx]; 
     }
 
-    T const & operator[](size_t idx) const { 
+    T const & operator[](unsigned idx) const { 
         SASSERT(idx < size()); 
         return m_data[idx];
     }
@@ -195,24 +195,24 @@ template<typename T>
 class ptr_array : public array<T *, false> {
 public:
     ptr_array() {}
-    ptr_array(void * mem, size_t sz, T * const * vs):array<T*, false>(mem, sz, vs) {}
+    ptr_array(void * mem, unsigned sz, T * const * vs):array<T*, false>(mem, sz, vs) {}
     template<typename Allocator>
-    ptr_array(Allocator & a, size_t sz, T * const * vs):array<T*, false>(a, sz, vs) {}
-    ptr_array(void * mem, size_t sz, bool init_mem):array<T*, false>(mem, sz, init_mem) {}
+    ptr_array(Allocator & a, unsigned sz, T * const * vs):array<T*, false>(a, sz, vs) {}
+    ptr_array(void * mem, unsigned sz, bool init_mem):array<T*, false>(mem, sz, init_mem) {}
     template<typename Allocator>
-    ptr_array(Allocator & a, size_t sz, bool init_mem):array<T*, false>(a, sz, init_mem) {}
+    ptr_array(Allocator & a, unsigned sz, bool init_mem):array<T*, false>(a, sz, init_mem) {}
 };
 
 template<typename T>
 class sarray : public array<T, false> {
 public:
     sarray() {}
-    sarray(void * mem, size_t sz, T const * vs):array<T, false>(mem, sz, vs) {}
+    sarray(void * mem, unsigned sz, T const * vs):array<T, false>(mem, sz, vs) {}
     template<typename Allocator>
-    sarray(Allocator & a, size_t sz, T const * vs):array<T, false>(a, sz, vs) {}
-    sarray(void * mem, size_t sz, bool init_mem):array<T, false>(mem, sz, init_mem) {}
+    sarray(Allocator & a, unsigned sz, T const * vs):array<T, false>(a, sz, vs) {}
+    sarray(void * mem, unsigned sz, bool init_mem):array<T, false>(mem, sz, init_mem) {}
     template<typename Allocator>
-    sarray(Allocator & a, size_t sz, bool init_mem):array<T, false>(a, sz, init_mem) {}
+    sarray(Allocator & a, unsigned sz, bool init_mem):array<T, false>(a, sz, init_mem) {}
 };
 
 #endif