Clean up occurrences of SmtEngine in comments. (#7349)

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 1222f3c9edeff8682857782dd4e3cda170688c8d..a9e5854b0be6cc24126bb0ce744e2acc4463b166 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -215,8 +215,8 @@ NodeManager::~NodeManager() {
 
   {
     ScopedBool dontGC(d_inReclaimZombies);
-    // hopefully by this point all SmtEngines have been deleted
-    // already, along with all their attributes
+    // By this point, all SolverEngines should have been deleted, along with
+    // all their attributes
     d_attrManager->deleteAllAttributes();
   }
 

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 204cdb677f44095c72aa1c7f875f2a022fb9e18d..b526efc80964aa1524cd024457d1066f469bc4ab 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -205,7 +205,7 @@ class NodeManager
 
   /**
    * Keep a count of all abstract values produced by this NodeManager.
-   * Abstract values have a type attribute, so if multiple SmtEngines
+   * Abstract values have a type attribute, so if multiple SolverEngines
    * are attached to this NodeManager, we don't want their abstract
    * values to overlap.
    */

diff --git a/src/smt/command.h b/src/smt/command.h
index 5df891ead869dcc357514babf91768d96062095d..400f3492e1263da15f62bf341e8581fd9880375c 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Implementation of the command pattern on SmtEngines.
+ * Implementation of the command pattern on SolverEngines.
  *
  * Command objects are generated by the parser (typically) to implement the
  * commands in parsed input (see Parser::parseNextCommand()), or by client

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index e522b45ddcaf1892fba15edef734da435a017c93..b08e6f298f8ca279b21e56d583cafcc71b687f09 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -339,7 +339,7 @@ bool ProcessAssertions::apply(Assertions& as)
     d_passes["bv-eager-atoms"]->apply(&assertions);
   }
 
-  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
+  Trace("smt-proc") << "ProcessAssertions::apply() end" << endl;
   dumpAssertions("post-everything", as);
 
   return noConflict;

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index f893c89d7113361069c4fe1af46f63b724218126..613942d19626625748fae21303cb4d9b7fcd4919 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -408,7 +408,7 @@ class RewriteRule {
 
   // /* Statistics about the rule */
   // // NOTE: Cannot have static fields like this, or else you can't have
-  // // two SmtEngines in the process (the second-to-be-destroyed will
+  // // two SolverEngines in the process (the second-to-be-destroyed will
   // // have a dangling pointer and segfault).  If this statistic is needed,
   // // fix the rewriter by making it an instance per-SolverEngine (instead of
   // // static).