diff options
| -rw-r--r-- | src/expr/node_manager.cpp | 4 | ||||
| -rw-r--r-- | src/expr/node_manager.h | 2 | ||||
| -rw-r--r-- | src/smt/command.h | 2 | ||||
| -rw-r--r-- | src/smt/process_assertions.cpp | 2 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 2 |
5 files changed, 6 insertions, 6 deletions
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). |