From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 12 Oct 2021 18:31:57 +0000 (-0700)
Subject: Clean up occurrences of SmtEngine in comments. (#7349)
X-Git-Tag: cvc5-1.0.0~1076
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=97c9e6ddc22ff53408154bc3f82dae40992606f2;p=cvc5.git

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

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 1222f3c9e..a9e5854b0 100644
--- 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 204cdb677..b526efc80 100644
--- 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 5df891ead..400f3492e 100644
--- 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 e522b45dd..b08e6f298 100644
--- 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 f893c89d7..613942d19 100644
--- 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).