| -lemma-out-file <string> | - | File to dump lemmas to [default=''''] |
| -lemma-in-file <string> | - | File to read lemmas from [default=''''] |
| -csv-trace-file <string> | - | File to save execution trace in |
| CSV format [default=''''] | ||
| -var-stat-file <string> | - | File to save var stats [default=''''] |
| -cvs-depth-breadth-file <string> | - | Save depth/breadth statistic [default=''''] |
| -backjumping <number> | - | Enable/Disable backjumping (1/0) |
| [default=1] | ||
| -max-cached-lemmas <number>, | - | Set the maximum # of lemmas |
| -L <number> | [default=5000] | |
| -autarky-smurfs <number> | - | Use Autarky Smurfs in the solver (1/0) |
| [default=0] | ||
| -autarky-lemmas <number> | - | Use Autarky Lemmas in the solver (Currently Unavailiable) (1/0) |
| [default=0] | ||
| -sbj <number> | - | Super backjumping [default=0] |
| -max-vbles-per-smurf <number>, | - | set the maximum number variables per |
| -S <number> | smurf [default=8] | |
| -backtracks-per-report <number> | - | set the number of backtracks per report |
| [default=10000] | ||
| -max-brancher-cp <number> | - | set the choice point limit (0=no limit) |
| [default=0] | ||
| -brancher-trace-start <number> | - | number of backtracks to start the trace |
| (when debug=9) [default=0] | ||
| -heuristic <string>, | - | Choose heuristic j=LSGB, l=Chaff-like |
| -H <string> | lemma based, i=Interactive [default="j"] | |
| -jheuristic-k <number>, | - | set the value of K [default=3.000000] |
| -K <number> | ||
| -jheuristic-k-true <number> | - | set the value of True state [default=0.000000] |
| -jheuristic-k-inf <number> | - | set the value of the inference multiplier |
| [default=1.000000] |