Print original form for substitutions and learned literals (#7959)

diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 7e8a543983927319fb5bf1cb6e614c6a9688403b..7d26b4ff0e1e3a086273404653a7b7fe9104c1c8 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -16,6 +16,7 @@
 #include "preprocessing/preprocessing_pass_context.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/base_options.h"
 #include "smt/env.h"
 #include "theory/theory_engine.h"
@@ -85,7 +86,7 @@ std::vector<Node> PreprocessingPassContext::getLearnedLiterals() const
 void PreprocessingPassContext::printSubstitution(const Node& lhs,
                                                  const Node& rhs) const
 {
-  Node eq = lhs.eqNode(rhs);
+  Node eq = SkolemManager::getOriginalForm(lhs.eqNode(rhs));
   output(OutputTag::LEARNED_LITS)
       << "(learned-lit " << eq << " :preprocess-subs)" << std::endl;
   output(OutputTag::SUBS) << "(substitution " << eq << ")" << std::endl;

diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp
index 1b11662aa0de994c7cb7f98ec46b62cb4dcfd522..3562545b89fcb87e9569ee12f7a866e8241503ee 100644 (file)
--- a/src/prop/zero_level_learner.cpp
+++ b/src/prop/zero_level_learner.cpp
@@ -84,7 +84,8 @@ void ZeroLevelLearner::notifyInputFormulas(
     for (const Node& lit : ppl)
     {
       output(OutputTag::LEARNED_LITS)
-          << "(learned-lit " << lit << " :preprocess)" << std::endl;
+          << "(learned-lit " << SkolemManager::getOriginalForm(lit)
+          << " :preprocess)" << std::endl;
     }
   }
   for (const Node& a : assertions)