From b5efb87118bad39bd0145be5992fd8d8e507b599 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 29 Nov 2021 19:55:10 -0800
Subject: [PATCH] base -> core

---
 src/solver/solver.h               | 2 +-
 src/tactic/tactic.h               | 4 ++--
 src/tactic/user_propagator_base.h | 5 ++---
 3 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/solver/solver.h b/src/solver/solver.h
index 90975ebf9a7..090cd9d9b71 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -48,7 +48,7 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p);
      - statistics
      - results based on check_sat_result API
 */
-class solver : public check_sat_result, public user_propagator::base{
+class solver : public check_sat_result, public user_propagator::core {
     params_ref  m_params;
     symbol      m_cancel_backup_file;
 public:
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index 37a211cb4f0..de04c945334 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -20,11 +20,11 @@ Module Name:
 --*/
 #pragma once
 
-#include "tactic/goal.h"
 #include "util/params.h"
+#include "util/lbool.h"
 #include "util/statistics.h"
+#include "tactic/goal.h"
 #include "tactic/tactic_exception.h"
-#include "util/lbool.h"
 
 class progress_callback;
 
diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h
index f7826e559c8..dd09efa0395 100644
--- a/src/tactic/user_propagator_base.h
+++ b/src/tactic/user_propagator_base.h
@@ -24,7 +24,7 @@ namespace user_propagator {
     typedef std::function<void(void*,unsigned)>        pop_eh_t;
 
 
-    class base {
+    class core {
     public:
         
         virtual void user_propagate_init(
@@ -33,8 +33,7 @@ namespace user_propagator {
             pop_eh_t&                                    pop_eh,
             fresh_eh_t&                                  fresh_eh) {
             throw default_exception("user-propagators are only supported on the SMT solver");
-        }
-        
+        }        
         
         virtual void user_propagate_register_fixed(fixed_eh_t& fixed_eh) {
             throw default_exception("user-propagators are only supported on the SMT solver");