Use symbol manager for unsat cores (#5468)

This PR uses the symbol manager for handling names for unsat cores.

This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.

1 files changed, 6 insertions, 4 deletions

diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index 75ffa4f62..a163e503d 100644
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -77,18 +77,20 @@ bool SymbolManager::Implementation::setExpressionName(api::Term t,
                                                       const std::string& name,
                                                       bool isAssertion)
 {
+  Trace("sym-manager") << "set expression name: " << t << " -> " << name
+                       << ", isAssertion=" << isAssertion << std::endl;
   // cannot name subexpressions under quantifiers
   PrettyCheckArgument(
       !d_hasPushedScope.get(), name, "cannot name function in a scope");
+  if (isAssertion)
+  {
+    d_namedAsserts.insert(t);
+  }
   if (d_names.find(t) != d_names.end())
   {
     // already named assertion
     return false;
   }
-  if (isAssertion)
-  {
-    d_namedAsserts.insert(t);
-  }
   d_names[t] = name;
   return true;
 }