From 227e6801c2276929c3b3242e97d23f55b993491f Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 24 Aug 2017 18:33:21 +0100
Subject: [PATCH] Whitespace

---
 src/tactic/ufbv/macro_finder_tactic.cpp | 44 ++++++++++++-------------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp
index 9b1835ff3..e1e3b669b 100644
--- a/src/tactic/ufbv/macro_finder_tactic.cpp
+++ b/src/tactic/ufbv/macro_finder_tactic.cpp
@@ -26,24 +26,24 @@ Notes:
 #include "tactic/extension_model_converter.h"
 #include "tactic/ufbv/macro_finder_tactic.h"
 
-class macro_finder_tactic : public tactic {    
+class macro_finder_tactic : public tactic {
 
     struct imp {
         ast_manager & m_manager;
         bool m_elim_and;
 
-        imp(ast_manager & m, params_ref const & p) : 
+        imp(ast_manager & m, params_ref const & p) :
             m_manager(m),
             m_elim_and(false) {
             updt_params(p);
         }
-        
+
         ast_manager & m() const { return m_manager; }
-        
-        
-        void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        model_converter_ref & mc, 
+
+
+        void operator()(goal_ref const & g,
+                        goal_ref_buffer & result,
+                        model_converter_ref & mc,
                         proof_converter_ref & pc,
                         expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
@@ -63,20 +63,20 @@ class macro_finder_tactic : public tactic {
             bv_simplifier_params bv_params;
             bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params);
             simp.register_plugin(bvsimp);
-                
+
             macro_manager mm(m_manager, simp);
             macro_finder mf(m_manager, mm);
-            
+
             expr_ref_vector forms(m_manager), new_forms(m_manager);
-            proof_ref_vector proofs(m_manager), new_proofs(m_manager);            
+            proof_ref_vector proofs(m_manager), new_proofs(m_manager);
             unsigned   size = g->size();
             for (unsigned idx = 0; idx < size; idx++) {
                 forms.push_back(g->form(idx));
-                proofs.push_back(g->pr(idx));                
+                proofs.push_back(g->pr(idx));
             }
 
             mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);
-        
+
             g->reset();
             for (unsigned i = 0; i < new_forms.size(); i++)
                 g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
@@ -89,7 +89,7 @@ class macro_finder_tactic : public tactic {
                 evmc->insert(f, f_interp);
             }
             mc = evmc;
-                        
+
             g->inc_depth();
             result.push_back(g.get());
             TRACE("macro-finder", g->display(tout););
@@ -102,7 +102,7 @@ class macro_finder_tactic : public tactic {
     };
 
     imp *      m_imp;
-    params_ref m_params;    
+    params_ref m_params;
 public:
     macro_finder_tactic(ast_manager & m, params_ref const & p):
         m_params(p) {
@@ -112,7 +112,7 @@ public:
     virtual tactic * translate(ast_manager & m) {
         return alloc(macro_finder_tactic, m, m_params);
     }
-        
+
     virtual ~macro_finder_tactic() {
         dealloc(m_imp);
     }
@@ -128,19 +128,19 @@ public:
         insert_produce_proofs(r);
         r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier.");
     }
-    
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            model_converter_ref & mc, 
+
+    virtual void operator()(goal_ref const & in,
+                            goal_ref_buffer & result,
+                            model_converter_ref & mc,
                             proof_converter_ref & pc,
                             expr_dependency_ref & core) {
         (*m_imp)(in, result, mc, pc, core);
     }
-    
+
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
         imp * d = alloc(imp, m, m_params);
-        std::swap(d, m_imp);        
+        std::swap(d, m_imp);
         dealloc(d);
     }