diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h
index e814afcb1..bc731bf9c 100644
--- a/src/smt/smt_quantifier.h
+++ b/src/smt/smt_quantifier.h
@@ -37,7 +37,7 @@ namespace smt {
     public:
         quantifier_manager(context & ctx, smt_params & fp, params_ref const & p);
         ~quantifier_manager();
-        
+
         context & get_context() const;
 
         void set_plugin(quantifier_manager_plugin * plugin);
@@ -51,12 +51,12 @@ namespace smt {
         quantifier_stat * get_stat(quantifier * q) const;
         unsigned get_generation(quantifier * q) const;
 
-        bool add_instance(quantifier * q, app * pat, 
-                          unsigned num_bindings, 
-                          enode * const * bindings, 
-                          unsigned max_generation, 
-                          unsigned min_top_generation, 
-                          unsigned max_top_generation, 
+        bool add_instance(quantifier * q, app * pat,
+                          unsigned num_bindings,
+                          enode * const * bindings,
+                          unsigned max_generation,
+                          unsigned min_top_generation,
+                          unsigned max_top_generation,
                           ptr_vector<enode> & used_enodes);
         bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0);
 
@@ -78,11 +78,11 @@ namespace smt {
 	bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
         void adjust_model(proto_model * m);
         check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value);
-        
+
         void push();
         void pop(unsigned num_scopes);
         void reset();
-        
+
         void display(std::ostream & out) const;
         void display_stats(std::ostream & out, quantifier * q) const;
 
@@ -97,7 +97,7 @@ namespace smt {
     public:
         quantifier_manager_plugin() {}
         virtual ~quantifier_manager_plugin() {}
-        
+
         virtual void set_manager(quantifier_manager & qm) = 0;
 
         virtual quantifier_manager_plugin * mk_fresh() = 0;
@@ -106,7 +106,7 @@ namespace smt {
         virtual void del(quantifier * q) = 0;
 
         virtual bool is_shared(enode * n) const = 0;
-        
+
         /**
            \brief This method is invoked whenever q is assigned to true.
         */
@@ -131,9 +131,9 @@ namespace smt {
            \brief This method is invoked whenever the solver restarts.
         */
         virtual void restart_eh() = 0;
-        
+
         /**
-           \brief Return true if the quantifier_manager can propagate information 
+           \brief Return true if the quantifier_manager can propagate information
            information back into the core.
         */
         virtual bool can_propagate() const = 0;
@@ -143,11 +143,11 @@ namespace smt {
            \brief Return true if the plugin is "model based"
          */
         virtual bool model_based() const = 0;
-        
+
         /**
            \brief Is "model based" instantiate allowed to instantiate this quantifier?
          */
-	virtual bool mbqi_enabled(quantifier *q) const {return true;}
+    	virtual bool mbqi_enabled(quantifier *q) const {return true;}
 
         /**
            \brief Give a change to the plugin to adjust the interpretation of unintepreted functions.
@@ -161,10 +161,10 @@ namespace smt {
            It also provides a mapping from enodes to their interpretations.
         */
         virtual quantifier_manager::check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value) = 0;
-        
+
         virtual void push() = 0;
         virtual void pop(unsigned num_scopes) = 0;
-        
+
     };
 };