(proof-new) Change proof-new option to proof (#5955)

Also moves several proof-specific options to proof_options.

26 files changed, 117 insertions, 131 deletions

diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index 665e68d28..2edad1647 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -17,7 +17,7 @@
 #include "expr/proof.h"
 #include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 
 namespace CVC4 {
 
@@ -261,8 +261,8 @@ void LazyCDProofChain::addLazyStep(Node expected,
                              << " set to generator " << pg->identify() << "\n";
   // note this will rewrite the generator for expected, if any
   d_gens.insert(expected, pg);
-  // check if chain is closed if options::proofNewEagerChecking() is on
-  if (options::proofNewEagerChecking())
+  // check if chain is closed if options::proofEagerChecking() is on
+  if (options::proofEagerChecking())
   {
     Trace("lazy-cdproofchain")
         << "LazyCDProofChain::addLazyStep: Checking closed proof...\n";
diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index a60a82b60..dc87d1795 100644
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -15,7 +15,7 @@
 #include "expr/proof_checker.h"
 
 #include "expr/skolem_manager.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 #include "smt/smt_statistics_registry.h"
 
 using namespace CVC4::kind;
@@ -243,7 +243,7 @@ Node ProofChecker::checkInternal(PfRule id,
     }
   }
   // fails if pedantic level is not met
-  if (options::proofNewEagerChecking())
+  if (options::proofEagerChecking())
   {
     std::stringstream serr;
     if (isPedanticFailure(id, serr, enableOutput))
@@ -251,11 +251,11 @@ Node ProofChecker::checkInternal(PfRule id,
       if (enableOutput)
       {
         out << serr.str() << std::endl;
-        if (Trace.isOn("proof-new-pedantic"))
+        if (Trace.isOn("proof-pedantic"))
         {
-          Trace("proof-new-pedantic")
+          Trace("proof-pedantic")
               << "Failed pedantic check for " << id << std::endl;
-          Trace("proof-new-pedantic") << "Expected: " << expected << std::endl;
+          Trace("proof-pedantic") << "Expected: " << expected << std::endl;
           out << "Expected: " << expected << std::endl;
         }
       }
@@ -334,10 +334,10 @@ bool ProofChecker::isPedanticFailure(PfRule id,
         out << "pedantic level for " << id << " not met (rule level is "
             << itp->second << " which is at or below the pedantic level "
             << d_pclevel << ")";
-        bool pedanticTraceEnabled = Trace.isOn("proof-new-pedantic");
+        bool pedanticTraceEnabled = Trace.isOn("proof-pedantic");
         if (!pedanticTraceEnabled)
         {
-          out << ", use -t proof-new-pedantic for details";
+          out << ", use -t proof-pedantic for details";
         }
       }
       return true;
diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp
index 14b7f06f1..6eebcd3ec 100644
--- a/src/expr/proof_ensure_closed.cpp
+++ b/src/expr/proof_ensure_closed.cpp
@@ -15,6 +15,7 @@
 #include "expr/proof_ensure_closed.h"
 
 #include "expr/proof_node_algorithm.h"
+#include "options/proof_options.h"
 #include "options/smt_options.h"
 
 namespace CVC4 {
@@ -31,13 +32,13 @@ void ensureClosedWrtInternal(Node proven,
                              const char* ctx,
                              bool reqGen)
 {
-  if (!options::proofNew())
+  if (!options::proof())
   {
     // proofs not enabled, do not do check
     return;
   }
   bool isTraceDebug = Trace.isOn(c);
-  if (!options::proofNewEagerChecking() && !isTraceDebug)
+  if (!options::proofEagerChecking() && !isTraceDebug)
   {
     // trace is off and proof new eager checking is off, do not do check
     return;
diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h
index 03ee1e717..7b970a71a 100644
--- a/src/expr/proof_ensure_closed.h
+++ b/src/expr/proof_ensure_closed.h
@@ -26,7 +26,7 @@ namespace CVC4 {
 /**
  * Debug check closed on Trace c. Context ctx is string for debugging.
  * This method throws an assertion failure if pg cannot provide a closed
- * proof for fact proven. This is checked only if --proof-new-eager-checking
+ * proof for fact proven. This is checked only if --proof-eager-checking
  * is enabled or the Trace c is enabled.
  *
  * @param reqGen Whether we consider a null generator to be a failure.
diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index c3e0aa5b0..2af296813 100644
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -103,7 +103,7 @@ void getFreeAssumptionsMap(
               != traversing.end())
           {
             Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use "
-                           "--proof-new-eager-checking)"
+                           "--proof-eager-checking)"
                         << std::endl;
           }
           visit.push_back(cp);
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index cacd2c101..f5e15f6d6 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/proof.h"
 #include "expr/proof_node_algorithm.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4::kind;
@@ -304,7 +304,7 @@ bool ProofNodeManager::updateNodeInternal(
 {
   Assert(pn != nullptr);
   // ---------------- check for cyclic
-  if (options::proofNewEagerChecking())
+  if (options::proofEagerChecking())
   {
     std::unordered_set<const ProofNode*> visited;
     for (const std::shared_ptr<ProofNode>& cpc : children)
diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index 71c75ceae..fbfc3e3d4 100644
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -56,7 +56,7 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
             != traversing.end())
         {
           Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use "
-                         "--proof-new-eager-checking)"
+                         "--proof-eager-checking)"
                       << std::endl;
           return Node::null();
         }
diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index 16e339645..e0f096075 100644
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -156,7 +156,7 @@ void ProofNodeUpdater::processInternal(
         {
           Unhandled()
               << "ProofNodeUpdater::processInternal: cyclic proof! (use "
-                 "--proof-new-eager-checking)"
+                 "--proof-eager-checking)"
               << std::endl;
         }
         visit.push_back(cp);
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index c744b237b..631a27604 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -10,3 +10,41 @@ header = "options/proof_options.h"
   default    = "false"
   read_only  = true
   help       = "Print conclusion of proof steps when printing AST"
+
+[[option]]
+  name       = "proofPedantic"
+  category   = "regular"
+  long       = "proof-pedantic=N"
+  type       = "uint32_t"
+  default    = "0"
+  read_only  = true
+  help       = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof"
+
+[[option]]
+  name       = "proofEagerChecking"
+  category   = "regular"
+  long       = "proof-eager-checking"
+  type       = "bool"
+  default    = "false"
+  help       = "check proofs eagerly with proof for local debugging"
+
+[[option]]
+  name       = "proofGranularityMode"
+  category   = "regular"
+  long       = "proof-granularity=MODE"
+  type       = "ProofGranularityMode"
+  default    = "THEORY_REWRITE"
+  help       = "modes for proof granularity"
+  help_mode  = "Modes for proof granularity."
+[[option.mode.OFF]]
+  name = "off"
+  help = "Do not improve the granularity of proofs."
+[[option.mode.REWRITE]]
+  name = "rewrite"
+  help = "Allow rewrite or substitution steps, expand macros."
+[[option.mode.THEORY_REWRITE]]
+  name = "theory-rewrite"
+  help = "Allow theory rewrite steps, expand macros, rewrite and substitution steps."
+[[option.mode.DSL_REWRITE]]
+  name = "dsl-rewrite"
+  help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps."
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index ed056ac9f..c29fe5e50 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -131,67 +131,28 @@ header = "options/smt_options.h"
   help = "Block models based on the concrete model values for the free variables."
 
 [[option]]
-  name       = "dumpProofs"
-  category   = "regular"
-  long       = "dump-proofs"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "output proofs after every UNSAT/VALID response"
-
-[[option]]
-  name       = "proofNew"
+  name       = "proof"
   category   = "regular"
-  long       = "proof-new"
+  long       = "proof"
   type       = "bool"
   default    = "false"
-  help       = "do proof production using the new infrastructure"
+  help       = "produce proofs, support check-proofs and get-proof"
 
 [[option]]
-  name       = "proofNewPedantic"
-  category   = "regular"
-  long       = "proof-new-pedantic=N"
-  type       = "uint32_t"
-  default    = "0"
-  read_only  = true
-  help       = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof-new"
-
-[[option]]
-  name       = "proofNewEagerChecking"
+  name       = "dumpProofs"
   category   = "regular"
-  long       = "proof-new-eager-checking"
+  long       = "dump-proofs"
   type       = "bool"
   default    = "false"
   read_only  = true
-  help       = "check proofs eagerly with proof-new for local debugging"
-
-[[option]]
-  name       = "proofGranularityMode"
-  category   = "regular"
-  long       = "proof-granularity=MODE"
-  type       = "ProofGranularityMode"
-  default    = "THEORY_REWRITE"
-  help       = "modes for proof granularity"
-  help_mode  = "Modes for proof granularity."
-[[option.mode.OFF]]
-  name = "off"
-  help = "Do not improve the granularity of proofs."
-[[option.mode.REWRITE]]
-  name = "rewrite"
-  help = "allow rewrite or substitution steps, expand macros."
-[[option.mode.THEORY_REWRITE]]
-  name = "theory-rewrite"
-  help = "allow theory rewrite steps, expand macros, rewrite and substitution steps."
-[[option.mode.DSL_REWRITE]]
-  name = "dsl-rewrite"
-  help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps."
+  help       = "output proofs after every UNSAT/VALID response"
 
 [[option]]
-  name       = "checkProofsNew"
+  name       = "checkProofs"
   category   = "regular"
-  long       = "check-proofs-new"
+  long       = "check-proofs"
   type       = "bool"
-  help       = "after UNSAT/VALID, check the generated proof (with proof-new)"
+  help       = "after UNSAT/VALID, check the generated proof (with proof)"
 
 [[option]]
   name       = "dumpInstantiations"
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 0a35e32eb..f788338be 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -57,7 +57,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
       imap[assertions->size()] = newSkolems[j];
       assertions->pushBackTrusted(newAsserts[j]);
       // new assertions have a dependence on the node (old pf architecture)
-      if (options::unsatCores() && !options::proofNew())
+      if (options::unsatCores() && !options::proof())
       {
         ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
                                                  assertion);
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index eef0326b6..840cb4c66 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -81,7 +81,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
     for( int i=0; i<(int)assertions.size(); i++ ){
       Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
       if( processAssertion( assertions[i] ) ){
-        if (options::unsatCores() && !options::proofNew()
+        if (options::unsatCores() && !options::proof()
             && std::find(macro_assertions.begin(),
                          macro_assertions.end(),
                          assertions[i])
@@ -107,7 +107,7 @@ bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
           // is an over-approximation. a more fine-grained unsat core
           // computation would require caching dependencies for each subterm of
           // the formula, which is expensive.
-          if (options::unsatCores() && !options::proofNew())
+          if (options::unsatCores() && !options::proof())
           {
             ProofManager::currentPM()->addDependence(curr, assertions[i]);
             for (unsigned j = 0; j < macro_assertions.size(); j++)
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index ab3b0cfe7..dbf734a3c 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -55,7 +55,7 @@ namespace {
  */
 bool assertionLevelOnly()
 {
-  return (options::proofNew() || options::unsatCores())
+  return (options::proof() || options::unsatCores())
          && options::incrementalSolving();
 }
 
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index c48df4998..d87b6fc45 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -160,7 +160,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
   }
   d_minisat->addClause(minisat_clause, removable, clause_id);
   // FIXME: to be deleted when we kill old proof code for unsat cores
-  Assert(!options::unsatCores() || options::proofNew()
+  Assert(!options::unsatCores() || options::proof()
          || clause_id != ClauseIdError);
   return clause_id;
 }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index e99e11eb2..738b4dc9c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -27,6 +27,7 @@
 #include "options/decision_options.h"
 #include "options/main_options.h"
 #include "options/options.h"
+#include "options/proof_options.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
 #include "prop/cnf_stream.h"
@@ -36,7 +37,6 @@
 #include "prop/theory_proxy.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/output_channel.h"
-#include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
@@ -205,7 +205,7 @@ void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
   Assert(ppSkolems.size() == ppLemmas.size());
 
   // do final checks on the lemmas we are about to send
-  if (isProofEnabled() && options::proofNewEagerChecking())
+  if (isProofEnabled() && options::proofEagerChecking())
   {
     Assert(tplemma.getGenerator() != nullptr);
     // ensure closed, make the proof node eagerly here to debug
@@ -444,7 +444,6 @@ Node PropEngine::ensureLiteral(TNode n)
 
 Node PropEngine::getPreprocessedTerm(TNode n)
 {
-  Node rewritten = theory::Rewriter::rewrite(n);
   // must preprocess
   std::vector<theory::TrustNode> newLemmas;
   std::vector<Node> newSkolems;
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index dd7e94f03..3def16b22 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -15,7 +15,7 @@
 #include "prop/sat_proof_manager.h"
 
 #include "expr/proof_node_algorithm.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/minisat/minisat.h"
 #include "theory/theory_proof_step_buffer.h"
@@ -650,7 +650,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
     }
   } while (expanded);
   // now we should be able to close it
-  if (options::proofNewEagerChecking())
+  if (options::proofEagerChecking())
   {
     std::vector<Node> assumptionsVec;
     for (const Node& a : d_assumptions)
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index beb2651bf..3065d6b07 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -81,7 +81,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
 
   theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
   Node theoryExplanation = tte.getNode();
-  if (CVC4::options::proofNew())
+  if (CVC4::options::proof())
   {
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index cb2887ec0..ef80ebdae 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -16,7 +16,7 @@
 #include "smt/preprocess_proof_generator.h"
 
 #include "expr/proof.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -235,7 +235,7 @@ std::string PreprocessProofGenerator::identify() const { return d_name; }
 
 void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
 {
-  if (options::proofNewEagerChecking())
+  if (options::proofEagerChecking())
   {
     // catch a pedantic failure now, which otherwise would not be
     // triggered since we are doing lazy proof generation
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index b8f68af88..cb7943aed 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/proof_node_algorithm.h"
 #include "options/base_options.h"
-#include "options/smt_options.h"
+#include "options/proof_options.h"
 #include "smt/assertions.h"
 #include "smt/defined_function.h"
 
@@ -24,7 +24,7 @@ namespace CVC4 {
 namespace smt {
 
 PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
-    : d_pchecker(new ProofChecker(options::proofNewPedantic())),
+    : d_pchecker(new ProofChecker(options::proofPedantic())),
       d_pnm(new ProofNodeManager(d_pchecker.get())),
       d_pppg(new PreprocessProofGenerator(
           d_pnm.get(), u, "smt::PreprocessProofGenerator")),
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index ab8dd8f92..0898096f5 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -15,6 +15,7 @@
 #include "smt/proof_post_processor.h"
 
 #include "expr/skolem_manager.h"
+#include "options/proof_options.h"
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "smt/smt_engine.h"
@@ -1110,7 +1111,7 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
 {
   PfRule r = pn->getRule();
   // if not doing eager pedantic checking, fail if below threshold
-  if (!options::proofNewEagerChecking())
+  if (!options::proofEagerChecking())
   {
     if (!d_pedanticFailure)
     {
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 93196fde4..98fbfe1b3 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -73,7 +73,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
   if (options::checkUnsatCoresNew())
   {
-    options::proofNew.set(true);
+    options::proof.set(true);
   }
   if (options::bitvectorAigSimplifications.wasSetByUser())
   {
@@ -872,16 +872,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
   if (options::ufHo())
   {
-    // if higher-order, disable proof production
-    if (options::proofNew())
-    {
-      if (options::proofNew.wasSetByUser())
-      {
-        Warning() << "SmtEngine: turning off proof production (not yet "
-                     "supported with --uf-ho)\n";
-      }
-      options::proofNew.set(false);
-    }
     // if higher-order, then current variants of model-based instantiation
     // cannot be used
     if (options::mbqiMode() != options::MbqiMode::NONE)
@@ -1095,16 +1085,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       options::nlExtTangentPlanes.set(true);
     }
-    // not compatible with proofs
-    if (options::proofNew())
-    {
-      if (options::proofNew.wasSetByUser())
-      {
-        Notice() << "SmtEngine: setting proof-new to false to support SyGuS"
-                 << std::endl;
-      }
-      options::proofNew.set(false);
-    }
   }
   // counterexample-guided instantiation for non-sygus
   // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
@@ -1394,10 +1374,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
         "division. "
         "Try --bv-div-zero-const to interpret division by zero as a constant.");
   }
-  // !!!!!!!!!!!!!!!! temporary, until proof-new is functional
-  if (options::proofNew())
+  // !!!!!!!!!!!!!!!! temporary, until proofs are functional
+  if (options::proof())
   {
-    throw OptionException("--proof-new is not yet supported.");
+    throw OptionException("--proof is not yet supported.");
   }
 
   if (logic == LogicInfo("QF_UFNRA"))
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 09d54d6d8..941fd111a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -22,11 +22,13 @@
 #include "base/modal_exception.h"
 #include "base/output.h"
 #include "decision/decision_engine.h"
+#include "expr/bound_var_manager.h"
 #include "expr/node.h"
 #include "options/base_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
 #include "options/printer_options.h"
+#include "options/proof_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "printer/printer.h"
@@ -56,10 +58,10 @@
 #include "smt/unsat_core_manager.h"
 #include "theory/quantifiers/instantiation_list.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 #include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
 #include "util/random.h"
 #include "util/resource_manager.h"
 
@@ -222,8 +224,11 @@ void SmtEngine::finishInit()
   d_optm->finishInit(d_logic, d_isInternalSubsolver);
 
   ProofNodeManager* pnm = nullptr;
-  if (options::proofNew())
+  if (options::proof())
   {
+    // ensure bound variable uses canonical bound variables
+    d_nodeManager->getBoundVarManager()->enableKeepCacheValues();
+    // make the proof manager
     d_pfManager.reset(new PfManager(getUserContext(), this));
     PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
     // start the unsat core manager
@@ -979,15 +984,15 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
       }
     }
     // Check that UNSAT results generate a proof correctly.
-    if (options::checkProofsNew() || options::proofNewEagerChecking())
+    if (options::checkProofs() || options::proofEagerChecking())
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
-        if ((options::checkProofsNew() || options::proofNewEagerChecking())
-            && !options::proofNew())
+        if ((options::checkProofs() || options::proofEagerChecking())
+            && !options::proof())
         {
           throw ModalException(
-              "Cannot check-proofs-new because proof-new was disabled.");
+              "Cannot check-proofs because proofs were disabled.");
         }
         checkProof();
       }
@@ -1398,13 +1403,17 @@ Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
 
 void SmtEngine::checkProof()
 {
-  Assert(options::proofNew());
+  Assert(options::proof());
   // internal check the proof
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
+  if (options::proofEagerChecking())
+  {
+    pe->checkProof(d_asserts->getAssertionList());
+  }
   Assert(pe->getProof() != nullptr);
   std::shared_ptr<ProofNode> pePfn = pe->getProof();
-  if (options ::checkProofsNew())
+  if (options::checkProofs())
   {
     d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions);
   }
@@ -1458,7 +1467,7 @@ void SmtEngine::checkUnsatCore() {
   initializeSubsolver(coreChecker);
   coreChecker->getOptions().set(options::checkUnsatCores, false);
   // disable all proof options
-  coreChecker->getOptions().set(options::proofNew, false);
+  coreChecker->getOptions().set(options::proof, false);
   coreChecker->getOptions().set(options::checkUnsatCoresNew, false);
 
   // set up separation logic heap if necessary
@@ -1536,9 +1545,9 @@ std::string SmtEngine::getProof()
         getOutputManager().getDumpOut());
   }
 #if IS_PROOFS_BUILD
-  if (!options::proofNew())
+  if (!options::proof())
   {
-    throw ModalException("Cannot get a proof when proof-new option is off.");
+    throw ModalException("Cannot get a proof when proof option is off.");
   }
   if (d_state->getMode() != SmtMode::UNSAT)
   {
@@ -1637,7 +1646,7 @@ void SmtEngine::getInstantiationTermVectors(
 {
   SmtScope smts(this);
   finishInit();
-  if (options::proofNew() && getSmtMode() == SmtMode::UNSAT)
+  if (options::proof() && getSmtMode() == SmtMode::UNSAT)
   {
     // TODO (project #37): minimize instantiations based on proof manager
   }
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 80e1ef8be..8b4d49f90 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -166,7 +166,7 @@ private:
    *   * assertionToEqualityEngine(..)
    *   * equalsConstant(c)
    *   * equalsConstant(lb, ub)
-   * If proofNew is off, then just asserts.
+   * If proof is off, then just asserts.
    */
   void assertLitToEqualityEngine(Node lit,
                                  TNode reason,
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index c1db8e55a..02580083b 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -1081,7 +1081,7 @@ TrustNode Constraint::split()
   Node lemma = NodeBuilder<3>(OR) << leqNode << geqNode;
 
   TrustNode trustedLemma;
-  if (options::proofNew())
+  if (d_database->isProofEnabled())
   {
     // Farkas proof that this works.
     auto nm = NodeManager::currentNM();
@@ -2068,7 +2068,7 @@ void ConstraintDatabase::proveOr(std::vector<TrustNode>& out,
   Node la = a->getLiteral();
   Node lb = b->getLiteral();
   Node orN = (la < lb) ? la.orNode(lb) : lb.orNode(la);
-  if (options::proofNew())
+  if (isProofEnabled())
   {
     Assert(b->getNegation()->getType() != ConstraintType::Disequality);
     auto nm = NodeManager::currentNM();
diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h
index 4760760ef..6f24d3601 100644
--- a/src/theory/arith/proof_macros.h
+++ b/src/theory/arith/proof_macros.h
@@ -20,15 +20,12 @@
 
 #include "options/smt_options.h"
 
-#define ARITH_PROOF(x)                                      \
-  if (CVC4::options::proofNew())                            \
-  {                                                         \
-    x;                                                      \
+#define ARITH_PROOF(x)        \
+  if (CVC4::options::proof()) \
+  {                           \
+    x;                        \
   }
-#define ARITH_NULLPROOF(x)                                  \
-  (CVC4::options::proofNew())                               \
-      ? x                                                   \
-      : NULL
-#define ARITH_PROOF_ON() CVC4::options::proofNew()
+#define ARITH_NULLPROOF(x) (CVC4::options::proof()) ? x : NULL
+#define ARITH_PROOF_ON() CVC4::options::proof()
 
 #endif  // CVC4__THEORY__ARITH__PROOF_MACROS_H
diff --git a/test/regress/regress0/arith/non-normal.smt2 b/test/regress/regress0/arith/non-normal.smt2
index 389bd6d2b..ccd0b7634 100644
--- a/test/regress/regress0/arith/non-normal.smt2
+++ b/test/regress/regress0/arith/non-normal.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --proof-new-eager-checking
+; COMMAND-LINE: --proof-eager-checking
 ; EXPECT: sat
 (set-logic QF_UFLRA)
 (declare-fun v1 () Real)