blob: a23241e3da751df17fea2d273fe5918ec73b6ca7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
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"
|
