3 files changed, 28 insertions, 3 deletions

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index bc701ebc8..ff437e7e6 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -997,7 +997,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
 
 Node ProofPostprocessCallback::addProofForWitnessForm(Node t, CDProof* cdp)
 {
-  Node tw = SkolemManager::getWitnessForm(t);
+  Node tw = SkolemManager::getOriginalForm(t);
   Node eq = t.eqNode(tw);
   if (t == tw)
   {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 94e53a093..3fdf67ed7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1523,6 +1523,19 @@ UnsatCore SmtEngine::getUnsatCore() {
   return getUnsatCoreInternal();
 }
 
+void SmtEngine::getRelevantInstantiationTermVectors(
+    std::map<Node, std::vector<std::vector<Node>>>& insts)
+{
+  Assert(d_state->getMode() == SmtMode::UNSAT);
+  // generate with new proofs
+  PropEngine* pe = getPropEngine();
+  Assert(pe != nullptr);
+  Assert(pe->getProof() != nullptr);
+  std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(
+      pe->getProof(), *d_asserts, *d_definedFunctions);
+  d_ucManager->getRelevantInstantiations(pfn, insts);
+}
+
 std::string SmtEngine::getProof()
 {
   Trace("smt") << "SMT getProof()\n";
@@ -1636,7 +1649,8 @@ void SmtEngine::getInstantiationTermVectors(
   finishInit();
   if (options::proof() && getSmtMode() == SmtMode::UNSAT)
   {
-    // TODO (project #37): minimize instantiations based on proof manager
+    // minimize instantiations based on proof manager
+    getRelevantInstantiationTermVectors(insts);
   }
   else
   {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 94c11be5b..56f3ffbb8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -527,7 +527,12 @@ class CVC4_PUBLIC SmtEngine
    */
   std::vector<Node> getValues(const std::vector<Node>& exprs);
 
-  /** Print all instantiations made by the quantifiers module.  */
+  /** print instantiations
+   *
+   * Print all instantiations for all quantified formulas on out,
+   * returns true if at least one instantiation was printed. The type of output
+   * (list, num, etc.) is determined by printInstMode.
+   */
   void printInstantiations(std::ostream& out);
   /**
    * Print the current proof. This method should be called after an UNSAT
@@ -665,6 +670,12 @@ class CVC4_PUBLIC SmtEngine
   void getInstantiationTermVectors(Node q,
                                    std::vector<std::vector<Node>>& tvecs);
   /**
+   * As above but only the instantiations that were relevant for the
+   * refutation.
+   */
+  void getRelevantInstantiationTermVectors(
+      std::map<Node, std::vector<std::vector<Node>>>& insts);
+  /**
    * Get instantiation term vectors, which maps each instantiated quantified
    * formula to the list of instantiations for that quantified formula. This
    * list is minimized if proofs are enabled, and this call is immediately