from meeting

12 files changed, 3 insertions, 3 deletions

diff --git a/src/core/prop_engine.h b/src/prop/prop_engine.h
index 0febd2927..0febd2927 100644
--- a/src/core/prop_engine.h
+++ b/src/prop/prop_engine.h
diff --git a/src/core/sat.h b/src/prop/sat.h
index 00a94c142..00a94c142 100644
--- a/src/core/sat.h
+++ b/src/prop/sat.h
diff --git a/src/core/prover.h b/src/smt/smt_engine.h
index 14eab7c03..6f6fb355a 100644
--- a/src/core/prover.h
+++ b/src/smt/smt_engine.h
@@ -25,7 +25,7 @@ namespace CVC4 {
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
-// Prover and override check()?
+// SmtEngine and override check()?
 //
 // Probably better than that is to have a configuration object that
 // indicates which passes are desired.  The configuration occurs
@@ -34,7 +34,7 @@ namespace CVC4 {
 //
 // The CNF conversion can go on in PropEngine.
 
-class Prover {
+class SmtEngine {
   /** Current set of assertions. */
   // TODO: make context-aware to handle user-level push/pop.
   std::vector<Expr> d_assertList;
@@ -107,7 +107,7 @@ public:
    * Pop a user-level context.  Throws an exception if nothing to pop.
    */
   void pop();
-};/* class Prover */
+};/* class SmtEngine */
 
 } /* CVC4 namespace */
 
diff --git a/src/core/assert.h b/src/util/assert.h
index a66503641..a66503641 100644
--- a/src/core/assert.h
+++ b/src/util/assert.h
diff --git a/src/core/command.h b/src/util/command.h
index 944b9c621..944b9c621 100644
--- a/src/core/command.h
+++ b/src/util/command.h
diff --git a/src/core/debug.h b/src/util/debug.h
index 36942d1ae..36942d1ae 100644
--- a/src/core/debug.h
+++ b/src/util/debug.h
diff --git a/src/core/decision_engine.h b/src/util/decision_engine.h
index 81d820eaa..81d820eaa 100644
--- a/src/core/decision_engine.h
+++ b/src/util/decision_engine.h
diff --git a/src/core/exception.h b/src/util/exception.h
index 792a98701..792a98701 100644
--- a/src/core/exception.h
+++ b/src/util/exception.h
diff --git a/src/core/literal.h b/src/util/literal.h
index 8b147c640..8b147c640 100644
--- a/src/core/literal.h
+++ b/src/util/literal.h
diff --git a/src/core/model.h b/src/util/model.h
index c07b75dfa..c07b75dfa 100644
--- a/src/core/model.h
+++ b/src/util/model.h
diff --git a/src/core/result.h b/src/util/result.h
index 50f488682..50f488682 100644
--- a/src/core/result.h
+++ b/src/util/result.h
diff --git a/src/core/unique_id.h b/src/util/unique_id.h
index 1a6f3427a..1a6f3427a 100644
--- a/src/core/unique_id.h
+++ b/src/util/unique_id.h