diff options
Diffstat (limited to 'src/options/proof_options.toml')
-rw-r--r-- | src/options/proof_options.toml | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml new file mode 100644 index 000000000..a23241e3d --- /dev/null +++ b/src/options/proof_options.toml @@ -0,0 +1,38 @@ +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" |