5 files changed, 2 insertions, 103 deletions
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 7c0aca100..e00db9393 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -3,44 +3,6 @@ name   = "Bitvector theory"
 header = "options/bv_options.h"
 
 [[option]]
-  name       = "bvProofFormat"
-  category   = "expert"
-  long       = "bv-proof-format=MODE"
-  type       = "BvProofFormat"
-  default    = "ER"
-  predicates = ["checkSatSolverEnabled<BvProofFormat>"]
-  help       = "choose which UNSAT proof format to use, see --bv-sat-solver=help"
-  help_mode  = "Bit-vector proof formats."
-[[option.mode.ER]]
-  name = "er"
-  help = "Extended Resolution, i.e. resolution with new variable definitions."
-[[option.mode.DRAT]]
-  name = "drat"
-  help = "Deletion and Resolution Asymmetric Tautology Additions."
-[[option.mode.LRAT]]
-  name = "lrat"
-  help = "DRAT with unit propagation hints to accelerate checking."
-
-[[option]]
-  name       = "bvOptimizeSatProof"
-  category   = "expert"
-  long       = "bv-optimize-sat-proof=MODE"
-  type       = "BvOptimizeSatProof"
-  default    = "FORMULA"
-  predicates = ["checkSatSolverEnabled<BvOptimizeSatProof>"]
-  help       = "enable SAT proof optimizations, see --bv-optimize-sat-proof=help"
-  help_mode  = "SAT proof optimization level."
-[[option.mode.NONE]]
-  name = "none"
-  help = "Do not optimize the SAT proof."
-[[option.mode.PROOF]]
-  name = "proof"
-  help = "Use drat-trim to shrink the SAT proof."
-[[option.mode.FORMULA]]
-  name = "formula"
-  help = "Use drat-trim to shrink the SAT proof and formula."
-
-[[option]]
   name       = "bvSatSolver"
   smt_name   = "bv-sat-solver"
   category   = "expert"
diff --git a/src/options/options.h b/src/options/options.h
index 44f4be7b4..abcf21264 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -150,7 +150,6 @@ public:
   options::InstFormatMode getInstFormatMode() const;
   OutputLanguage getOutputLanguage() const;
   bool getUfHo() const;
-  bool getCheckProofs() const;
   bool getDumpInstantiations() const;
   bool getDumpModels() const;
   bool getDumpProofs() const;
@@ -167,7 +166,6 @@ public:
   bool getMemoryMap() const;
   bool getParseOnly() const;
   bool getProduceModels() const;
-  bool getProof() const;
   bool getSegvSpin() const;
   bool getSemanticChecks() const;
   bool getStatistics() const;
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index c8104c584..2dc28b10d 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -54,10 +54,6 @@ OutputLanguage Options::getOutputLanguage() const {
 
 bool Options::getUfHo() const { return (*this)[options::ufHo]; }
 
-bool Options::getCheckProofs() const{
-  return (*this)[options::checkProofs];
-}
-
 bool Options::getDumpInstantiations() const{
   return (*this)[options::dumpInstantiations];
 }
@@ -124,10 +120,6 @@ bool Options::getProduceModels() const{
   return (*this)[options::produceModels];
 }
 
-bool Options::getProof() const{
-  return (*this)[options::proof];
-}
-
 bool Options::getSegvSpin() const{
   return (*this)[options::segvSpin];
 }
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index a23241e3d..9db541e27 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -1,38 +1,3 @@
 id     = "PROOF"
 name   = "Proof"
 header = "options/proof_options.h"
-
-[[option]]
-  name       = "lfscLetification"
-  category   = "regular"
-  long       = "lfsc-letification"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "turns on global letification in LFSC proofs"
-
-[[option]]
-  name       = "aggressiveCoreMin"
-  category   = "regular"
-  long       = "aggressive-core-min"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "turns on aggressive unsat core minimization (experimental)"
-
-[[option]]
-  name       = "fewerPreprocessingHoles"
-  category   = "regular"
-  long       = "fewer-preprocessing-holes"
-  type       = "bool"
-  default    = "false"
-  help       = "try to eliminate preprocessing holes in proofs"
-
-[[option]]
-  name       = "allowEmptyDependencies"
-  category   = "regular"
-  long       = "allow-empty-dependencies"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "if unable to track the dependencies of a rewritten/preprocessed assertion, fail silently"
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 6b5bee6bb..2c87158de 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -131,24 +131,6 @@ header = "options/smt_options.h"
   help = "Block models based on the concrete model values for the free variables."
 
 [[option]]
-  name       = "proof"
-  smt_name   = "produce-proofs"
-  category   = "regular"
-  long       = "proof"
-  type       = "bool"
-  default    = "false"
-  predicates = ["proofEnabledBuild"]
-  help       = "turn on proof generation"
-
-[[option]]
-  name       = "checkProofs"
-  category   = "regular"
-  long       = "check-proofs"
-  type       = "bool"
-  predicates = ["LFSCEnabledBuild"]
-  help       = "after UNSAT/VALID, machine-check the generated proof"
-
-[[option]]
   name       = "dumpProofs"
   category   = "regular"
   long       = "dump-proofs"
@@ -390,7 +372,7 @@ header = "options/smt_options.h"
   type       = "bool"
   default    = "false"
   help       = "calculate sort inference of input problem, convert the input based on monotonic sorts"
-  
+
 [[option]]
   name       = "incrementalSolving"
   category   = "common"
@@ -660,7 +642,7 @@ header = "options/smt_options.h"
   [[option.mode.BITWISE]]
   name = "bitwise"
   help = "use bitwise comparisons on binary representation of integer for refinement (experimental)"
-  
+
 [[option]]
   name       = "solveIntAsBV"
   category   = "undocumented"