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

Also moves several proof-specific options to proof_options.

1 files changed, 9 insertions, 48 deletions

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"