diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 8df4234fa..dd48ef727 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -115,7 +115,7 @@ protected:
     func_decl * m_i_div_decl;
     func_decl * m_i_mod_decl;
     func_decl * m_i_rem_decl;
-    
+
     func_decl * m_to_real_decl;
     func_decl * m_to_int_decl;
     func_decl * m_is_int_decl;
@@ -140,7 +140,7 @@ protected:
 
     app       * m_pi;
     app       * m_e;
- 
+
     app       * m_0_pw_0_int;
     app       * m_0_pw_0_real;
     func_decl * m_neg_root_decl;
@@ -149,7 +149,7 @@ protected:
     func_decl * m_mod_0_decl;
     func_decl * m_u_asin_decl;
     func_decl * m_u_acos_decl;
-   
+
     ptr_vector<app> m_small_ints;
     ptr_vector<app> m_small_reals;
 
@@ -175,11 +175,11 @@ public:
     }
 
     virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
-    
-    virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+
+    virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                      unsigned arity, sort * const * domain, sort * range);
 
-    virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+    virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                      unsigned num_args, expr * const * args, sort * range);
 
     virtual bool is_value(app * e) const;
@@ -202,11 +202,11 @@ public:
     app * mk_numeral(sexpr const * p, unsigned i);
 
     app * mk_pi() const { return m_pi; }
-    
+
     app * mk_e() const { return m_e; }
 
     app * mk_0_pw_0_int() const { return m_0_pw_0_int; }
-    
+
     app * mk_0_pw_0_real() const { return m_0_pw_0_real; }
 
     virtual expr * get_some_value(sort * s);
@@ -258,7 +258,7 @@ public:
     bool is_to_int(expr const * n) const { return is_app_of(n, m_afid, OP_TO_INT); }
     bool is_is_int(expr const * n) const { return is_app_of(n, m_afid, OP_IS_INT); }
     bool is_power(expr const * n) const { return is_app_of(n, m_afid, OP_POWER); }
-    
+
     bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); }
     bool is_int(expr const * n) const { return is_int(get_sort(n)); }
     bool is_real(sort const * s) const { return is_sort_of(s, m_afid, REAL_SORT); }
@@ -275,7 +275,7 @@ public:
     MATCH_BINARY(is_le);
     MATCH_BINARY(is_ge);
     MATCH_BINARY(is_lt);
-    MATCH_BINARY(is_gt);    
+    MATCH_BINARY(is_gt);
     MATCH_BINARY(is_mod);
     MATCH_BINARY(is_rem);
     MATCH_BINARY(is_div);
@@ -297,25 +297,25 @@ class arith_util : public arith_recognizers {
         SASSERT(m_plugin != 0);
         return *m_plugin;
     }
-    
+
 public:
     arith_util(ast_manager & m);
 
     ast_manager & get_manager() const { return m_manager; }
 
-    algebraic_numbers::manager & am() { 
-        return plugin().am(); 
+    algebraic_numbers::manager & am() {
+        return plugin().am();
     }
 
     bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
     bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
     algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
-    
+
     sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); }
     sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); }
 
-    app * mk_numeral(rational const & val, bool is_int) const { 
-        return plugin().mk_numeral(val, is_int); 
+    app * mk_numeral(rational const & val, bool is_int) const {
+        return plugin().mk_numeral(val, is_int);
     }
     app * mk_numeral(rational const & val, sort const * s) const {
         SASSERT(is_int(s) || is_real(s));
@@ -379,9 +379,9 @@ public:
     app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); }
     app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); }
     app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); }
-    
+
     /**
-       \brief Return the equality (= lhs rhs), but it makes sure that 
+       \brief Return the equality (= lhs rhs), but it makes sure that
        if one of the arguments is a numeral, then it will be in the right-hand-side;
        if none of them are numerals, then the left-hand-side has a smaller id than the right hand side.
     */