diff --git a/src/ast/rewriter/maximize_ac_sharing.cpp b/src/ast/rewriter/maximize_ac_sharing.cpp
index d7e8df7a2..a838f59fa 100644
--- a/src/ast/rewriter/maximize_ac_sharing.cpp
+++ b/src/ast/rewriter/maximize_ac_sharing.cpp
@@ -54,13 +54,13 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr
     TRACE("ac_sharing_detail", tout << "args: "; for (unsigned i = 0; i < num_args; i++) tout << mk_pp(_args[i], m) << "\n";);
     try_to_reuse:
     if (num_args > 1 && num_args < MAX_NUM_ARGS_FOR_OPT) {
-        for (unsigned i = 0; i < num_args - 1; i++) {
+        for (unsigned i = 0; i + 1 < num_args; i++) {
             for (unsigned j = i + 1; j < num_args; j++) {
                 if (contains(f, _args[i], _args[j])) {
                     TRACE("ac_sharing_detail", tout << "reusing args: " << i << " " << j << "\n";);
                     _args[i] = m.mk_app(f, _args[i], _args[j]);
                     SASSERT(num_args > 1);
-                    for (unsigned w = j; w < num_args - 1; w++) {
+                    for (unsigned w = j; w + 1 < num_args; w++) {
                         _args[w] = _args[w+1];
                     }
                     num_args--;
@@ -144,6 +144,7 @@ void maximize_ac_sharing::restore_entries(unsigned old_lim) {
     while (i != old_lim) {
         --i;
         entry * e = m_entries[i];
+        m_cache.remove(e);
         m.dec_ref(e->m_arg1);
         m.dec_ref(e->m_arg2);
     }
diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h
index e5a02953b..639d3e6a8 100644
--- a/src/sat/sat_watched.h
+++ b/src/sat/sat_watched.h
@@ -109,10 +109,10 @@ namespace sat {
         bool operator!=(watched const & w) const { return !operator==(w); }
     };
 
-    COMPILE_TIME_ASSERT(0 <= watched::BINARY && watched::BINARY <= 3);
-    COMPILE_TIME_ASSERT(0 <= watched::TERNARY && watched::TERNARY <= 3);
-    COMPILE_TIME_ASSERT(0 <= watched::CLAUSE && watched::CLAUSE <= 3);
-    COMPILE_TIME_ASSERT(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3);
+    static_assert(0 <= watched::BINARY && watched::BINARY <= 3, "");
+    static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, "");
+    static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, "");
+    static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, "");
 
     struct watched_lt {
         bool operator()(watched const & w1, watched const & w2) const {
diff --git a/src/smt/smt_theory_var_list.h b/src/smt/smt_theory_var_list.h
index d7e246824..aa2816786 100644
--- a/src/smt/smt_theory_var_list.h
+++ b/src/smt/smt_theory_var_list.h
@@ -67,9 +67,9 @@ namespace smt {
     };
 
     // 32 bit machine
-    COMPILE_TIME_ASSERT(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int)); 
+    static_assert(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int), "32 bit"); 
     // 64 bit machine
-    COMPILE_TIME_ASSERT(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int)); 
+    static_assert(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int), "64 bit"); 
 };
 
 #endif /* SMT_THEORY_VAR_LIST_H_ */
diff --git a/src/util/approx_set.h b/src/util/approx_set.h
index e696d52ee..1cb7ae9f2 100644
--- a/src/util/approx_set.h
+++ b/src/util/approx_set.h
@@ -29,7 +29,7 @@ public:
     static const unsigned long long zero = 0ull;
     static const unsigned long long one  = 1ull;
 };
-COMPILE_TIME_ASSERT(sizeof(unsigned long long) == 8);
+static_assert(sizeof(unsigned long long) == 8, "");
 
 template <> class approx_set_traits<unsigned> {
 public:
@@ -37,7 +37,7 @@ public:
     static const unsigned zero = 0;
     static const unsigned one  = 1;
 };
-COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
+static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes");
 
 template<typename T, typename T2U_Proc, typename R=unsigned long long>
 class approx_set_tpl : private T2U_Proc {
diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h
index 6a254e399..2d42e35a2 100644
--- a/src/util/bit_vector.h
+++ b/src/util/bit_vector.h
@@ -24,7 +24,7 @@ Revision History:
 #include "util/vector.h"
 #include "util/memory_manager.h"
 
-COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
+static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes");
 #define BV_DEFAULT_CAPACITY 2
 
 class bit_vector {
diff --git a/src/util/debug.h b/src/util/debug.h
index e0ceb9a64..536df4588 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -90,7 +90,6 @@ bool is_debug_enabled(const char * tag);
         exit(-1);                                           \
     }
 
-#define COMPILE_TIME_ASSERT(expr) static_assert(expr, "")
 
 void finalize_debug();
 /*
diff --git a/src/util/double_manager.h b/src/util/double_manager.h
index 33cccf2af..7532a3b8b 100644
--- a/src/util/double_manager.h
+++ b/src/util/double_manager.h
@@ -97,7 +97,7 @@ public:
     }
 };
 
-COMPILE_TIME_ASSERT(sizeof(uint64) == sizeof(double));
+static_assert(sizeof(uint64) == sizeof(double), "");
 
 #endif /* DOUBLE_MANAGER_H_ */
 
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index 5e7233110..3218419a9 100644
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@@ -73,7 +73,7 @@ mpf_manager::~mpf_manager() {
 }
 
 void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, int value) {
-    COMPILE_TIME_ASSERT(sizeof(int) == 4);
+    static_assert(sizeof(int) == 4, "assume integers are 4 bytes");
 
     o.sign = false;
     o.ebits = ebits;
@@ -119,7 +119,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
 
 void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) {
     // double === mpf(11, 53)
-    COMPILE_TIME_ASSERT(sizeof(double) == 8);
+    static_assert(sizeof(double) == 8, "doubles are 8 bytes");
 
     uint64 raw;
     memcpy(&raw, &value, sizeof(double));
@@ -155,7 +155,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) {
 
 void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, float value) {
     // single === mpf(8, 24)
-    COMPILE_TIME_ASSERT(sizeof(float) == 4);
+    static_assert(sizeof(float) == 4, "floats are 4 bytes");
 
     unsigned int raw;
     memcpy(&raw, &value, sizeof(float));
diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp
index 459b0691c..eac9cc80c 100644
--- a/src/util/mpff.cpp
+++ b/src/util/mpff.cpp
@@ -27,8 +27,8 @@ Revision History:
 #include "util/bit_util.h"
 #include "util/trace.h"
 
-COMPILE_TIME_ASSERT(sizeof(mpn_digit) == sizeof(unsigned));
-COMPILE_TIME_ASSERT(sizeof(unsigned)  == 4);
+static_assert(sizeof(mpn_digit) == sizeof(unsigned), "");
+static_assert(sizeof(unsigned)  == 4, "unsigned haven't changed size for a while");
 
 // MIN_MSW is an shorthand for 0x8000..00, i.e., the minimal most significand word.
 #define MIN_MSW (1u << (sizeof(unsigned) * 8 - 1))
diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp
index 65223133f..2059ea6fd 100644
--- a/src/util/mpn.cpp
+++ b/src/util/mpn.cpp
@@ -24,7 +24,7 @@ Revision History:
 #define max(a,b)    (((a) > (b)) ? (a) : (b))
 
 typedef uint64 mpn_double_digit;
-COMPILE_TIME_ASSERT(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit));
+static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment");
 
 const mpn_digit mpn_manager::zero = 0;
 
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 7cf87b24b..7ad472ef1 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -558,7 +558,7 @@ void mpz_manager<SYNCH>::big_rem(mpz const & a, mpz const & b, mpz & c) {
 
 template<bool SYNCH>
 void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
-    COMPILE_TIME_ASSERT(sizeof(a.m_val) == sizeof(int));
+    static_assert(sizeof(a.m_val) == sizeof(int), "size mismatch");
     if (is_small(a) && is_small(b) && a.m_val != INT_MIN && b.m_val != INT_MIN) {
         int _a = a.m_val;
         int _b = b.m_val;
@@ -724,7 +724,7 @@ void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
 
 #ifdef LEHMER_GCD
         // For now, it only works if sizeof(digit_t) == sizeof(unsigned)
-        COMPILE_TIME_ASSERT(sizeof(digit_t) == sizeof(unsigned));
+        static_assert(sizeof(digit_t) == sizeof(unsigned), "");
         
         int64 a_hat, b_hat, A, B, C, D, T, q, a_sz, b_sz;
         mpz a1, b1, t, r, tmp;
@@ -1754,7 +1754,7 @@ void mpz_manager<SYNCH>::mul2k(mpz & a, unsigned k) {
 }
 
 #ifndef _MP_GMP
-COMPILE_TIME_ASSERT(sizeof(digit_t) == 4 || sizeof(digit_t) == 8);
+static_assert(sizeof(digit_t) == 4 || sizeof(digit_t) == 8, "");
 #endif
 
 template<bool SYNCH>
@@ -1821,7 +1821,7 @@ unsigned mpz_manager<SYNCH>::log2(mpz const & a) {
     if (is_small(a))
         return ::log2((unsigned)a.m_val);
 #ifndef _MP_GMP
-    COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4);
+    static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, "");
     mpz_cell * c     = a.m_ptr;
     unsigned sz      = c->m_size;
     digit_t * ds     = c->m_digits; 
@@ -1843,7 +1843,7 @@ unsigned mpz_manager<SYNCH>::mlog2(mpz const & a) {
     if (is_small(a))
         return ::log2((unsigned)-a.m_val);
 #ifndef _MP_GMP
-    COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4);
+    static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, "");
     mpz_cell * c     = a.m_ptr;
     unsigned sz      = c->m_size;
     digit_t * ds     = c->m_digits; 
diff --git a/src/util/uint_set.h b/src/util/uint_set.h
index 33c39eeb2..352189ef1 100644
--- a/src/util/uint_set.h
+++ b/src/util/uint_set.h
@@ -22,7 +22,6 @@ Revision History:
 #include "util/util.h"
 #include "util/vector.h"
 
-COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
 
 class uint_set : unsigned_vector {
 
diff --git a/src/util/util.h b/src/util/util.h
index 23c2c1657..1f753099c 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -33,13 +33,13 @@ Revision History:
 typedef unsigned long long uint64;
 #endif
 
-COMPILE_TIME_ASSERT(sizeof(uint64) == 8);
+static_assert(sizeof(uint64) == 8, "64 bits please");
 
 #ifndef int64
 typedef long long int64;
 #endif
 
-COMPILE_TIME_ASSERT(sizeof(int64) == 8);
+static_assert(sizeof(int64) == 8, "64 bits");
 
 #ifndef INT64_MIN
 #define INT64_MIN static_cast<int64>(0x8000000000000000ull)
@@ -111,7 +111,7 @@ inline unsigned next_power_of_two(unsigned v) {
 unsigned log2(unsigned v);
 unsigned uint64_log2(uint64 v);
 
-COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
+static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits");
 
 // Return the number of 1 bits in v.
 static inline unsigned get_num_1bits(unsigned v) {