Command-line options and output#
Run ./build/primo --help for the complete option inventory of your binary.
The captured help belongs to the
documented implementation; source metadata is centralized in the review ledger. This page explains the
common controls; the complete captured inventory below supplies accepted values and defaults.
Effective policies explains automatic selection and option dependencies.
Everyday use#
Option |
Default |
Use and boundary |
|---|---|---|
|
Off |
Print grouped CLI help and exit. |
|
Off |
Print revision/build information and exit. |
|
Off |
Suppress the startup banner; SMT-LIB responses remain enabled. |
|
Off |
Write query statistics to stderr. See Statistics reference. |
|
Off |
Check original assertions against a requested model. Set |
|
|
Choose |
|
|
Choose |
|
|
Enable or disable arithmetic phase hints; see Automatic QF_LRA heuristics. |
|
|
Enable or disable one-sided Real elimination under the same policy; assumptions sessions reject explicit enabling. |
|
Unlimited |
Positive budget, up to 1,000,000,000. Counts aggregate SMT-reported conflicts across supported routes; see conflict-limit accounting. Exhaustion returns |
|
|
Bound integer branch-and-bound nodes; reaching the bound can return |
|
|
Cooperative cancellation grace period after SIGINT/SIGTERM, from 1 to 3600 seconds. This is not a solve-time limit. |
For example:
./build/primo --quiet --stats docs/examples/first-solve.smt2
./build/primo --quiet --check-model docs/examples/model.smt2
./build/primo --quiet --incremental-mode=assumptions docs/examples/session.smt2
Options accept only their declared values/ranges. A name beginning with
experimental or a diagnostic switch does not identify a qualified default.
For component-specific controls, use Preprocessing,
EUF: congruence, explanations, and rollback, Linear real arithmetic, Quantifiers: binders and instantiation, and
Effective policies and option dependencies. The help snapshot includes every registered CLI
option; the prose above is intentionally a practical subset.
The two automatic-budget options, --euf-prop-budget and --euf-prop-delivery,
accept exactly auto, unlimited, or unsigned decimal digits fitting in
std::size_t. Zero and leading zeros are accepted; signs, whitespace, trailing
characters and overflow are CLI errors detected before solving by
parse_auto_budget. The options’
different zero meanings are described in effective policies.
Preprocessing diagnostic#
--preprocess-only stops before search. Use it with --stats to inspect
preprocessing cost and formula-size counters independently of solving. It
returns unsat if ground preprocessing proves a contradiction and unknown
otherwise, including when simplification leaves no assertions. It does not
print the transformed formula. With quantified UF input it stops after the
frontend: ground preprocessing does not support binders, and neither
instantiation nor SAT/theory search runs. Unsupported inputs remain unsupported.
The option defaults off and is not accepted in assumptions mode.
Output and exit status#
SMT-LIB answers, models and errors go to stdout. Diagnostics, startup information
and optional statistics go to stderr. Use --quiet when scripting.
The command loop returns zero when it finishes without a command/unsupported
failure; this includes normal sat, unsat and unknown responses. It returns
2 for a command error or an unsupported command/solving result. File-opening and
most explicit option-validation failures return 1. The incompatible combination
of --qf-uflra-online-euf and --model-equality-branching returns 2; CLI parsing
can return its own nonzero status. Cancellation and external termination need separate treatment.
An exit code alone never distinguishes SAT from UNSAT.
Each input file creates a fresh session. A command error stops the current
stream; an unsupported response marks a nonzero status but can allow later
commands to be processed. For reliable automation, capture the full response
sequence and stderr, and identify which check-sat each answer belongs to.
These conventions come from src/main.cpp and src/cli/response_printer.cpp.
Where defaults live#
CLI registration and validation currently live in src/main.cpp, enum spellings in src/cli/option_names.hpp, and solver defaults in src/smt/check_sat.hpp. Strategy selection can determine whether a particular option takes effect. The placeholder src/cli/options.cpp and src/cli/options.hpp are not the authoritative option implementation.
The documentation example checker compares the captured help with the built binary. Update the help snapshot only after reviewing changed defaults and the affected manual pages; it is evidence for this revision, not a substitute for explaining new behavior.
Complete CLI inventory#
The snapshot is checked by the existing documentation example checker. The word “scaffold” in the banner is the current CLI description, not a capability classification. Experimental split counts are bounded by the available atoms, as explained in tactics.
Primo SMT solver scaffold
primo [OPTIONS] [files...]
POSITIONALS:
files FILE ... SMT-LIB input files. Reads stdin when omitted
Procedural options:
-h, --help Print this help message and exit
--check-model Check original assertions against produced typed models
-q, --quiet [default: off]
Suppress startup version banner
--stats [default: off]
Print solver statistics to stderr
--preprocess-only [default: off]
Diagnostic: stop before search; report unsat if preprocessing
refutes, otherwise unknown. Quantified input stops after the
frontend
--cancel-grace-seconds UINT:UINT in [1 - 3600] [1]
Seconds SIGTERM or SIGINT waits for the cooperative cancellation
path, which reports statistics, before answering unknown and
exiting
--version Display program version information and exit
Experimental tactic options:
--experimental-split-bools UINT:INT in [0 - 16] [0]
EXPERIMENTAL: split on up to k Boolean atoms, materialize 2^k
disjunctive goals, and solve them sequentially in false-first
order; 0 disables
--experimental-generic-model-combination [default: off]
Route QF_UFLRA shared-model decisions through the generic
sequential coordinator
QF_UF / EUF theory options:
--uf-symmetry-breaking [default: on]
Enable QF_UF symmetry breaking over invariant finite-domain
values
--no-uf-symmetry-breaking [default: off]
Disable QF_UF finite-domain symmetry breaking
--finite-domain-value-precedence [default: on]
Enable fixed-term value precedence inside finite-domain symmetry
breaking
--no-finite-domain-value-precedence [default: off]
Disable fixed-term value precedence inside finite-domain symmetry
breaking
--finite-domain-equality-definitions [default: off]
Enable guarded finite-domain equality definitions in auto
preprocessing
--no-finite-domain-equality-definitions [default: off]
Disable finite-domain SAT-visible equality definition clauses
--no-finite-domain-post-amo [default: off]
Disable the post-simplification finite-domain AMO scan
--quantifier-instance-simplification [default: on]
Quantified UF: normalize instances before duplicate detection
--no-quantifier-instance-simplification [default: off]
Quantified UF: compare and assert instances as instantiated
--eq-bridge [default: on]
Add equalities implied by every branch of selected QF_UF
disjunctions
--no-eq-bridge [default: off]
Disable equality bridging unless required by the preprocessing
preset
--ground-congruence [default: off]
Enable bounded SAT-visible ground congruence clauses
--ground-unit-substitution [default: off]
Enable experimental ground substitution from visible unit
equalities
--guarded-ground-unit-substitution [default: off]
Enable guarded ground substitution only when preprocessing
metrics predict a win
--no-solved-constant-substitution [default: off]
Disable QF_UF solved-constant substitution
--auto-basic-compact-term-limit UINT:INT in [0 - 100000000] [20000]
Maximum reachable terms for compact-clause basic auto
preprocessing; 0 means unlimited
--auto-basic-compact-min-conjuncts UINT:INT in [1 - 100000000] [2]
Minimum implicit top-level conjunct occurrences for
compact-clause basic auto preprocessing
--auto-basic-single-term-limit UINT:INT in [0 - 100000000] [15000]
Maximum reachable terms for finite-domain basic auto
preprocessing; 0 means unlimited
--auto-basic-single-min-domains UINT:INT in [1 - 100000000] [200]
Minimum recognized finite domains for finite-domain basic auto
preprocessing
--auto-basic-single-max-symmetry-terms UINT:INT in [0 - 100000000] [6]
Maximum terms in the accepted finite-domain symmetry group; 0
means unlimited
--no-auto-basic-single [default: off]
Disable the guarded auto basic-single preprocessing selector
--no-auto-basic-single-predicate-polarity [default: off]
Disable polarity phase for auto basic-single formulas with
Boolean UF predicates
--auto-basic-multi [default: on]
Enable the experimental auto basic-multi preprocessing and phase
heuristic
--no-auto-basic-multi [default: off]
Disable the auto basic-multi preprocessing and phase heuristic
--no-auto-basic-multi-polarity [default: off]
Disable polarity phase for auto basic-multi formulas
--qf-uf-profile TEXT:{default,tuned-interesting} [default]
QF_UF profile: default or tuned-interesting
--qf-uf-portfolio TEXT:{off,basic-polarity} [off]
QF_UF portfolio mode
--qf-uf-portfolio-conflicts UINT:INT in [1 - 1000000000] [2000]
Theory-conflict budget for the first QF_UF portfolio attempt
--euf-prop TEXT:{auto,off,conflict,model,online} [auto]
EUF propagation mode
--euf-engine TEXT:{lazy,incremental} [incremental]
EUF engine
--euf-explain-search TEXT:{one-sided,bidirectional,proof-forest,reoriented-proof-forest,structural-proof-forest} [one-sided]
Incremental EUF explanation search
--euf-proof-forest-diagnostics [default: off]
Record proof-forest path counters for incremental EUF
explanations
--euf-diseq-prop-diagnostics [default: off]
Record diagnostic-only QF_UF app-disequality propagation
opportunity counters
--euf-ackermann-diagnostics [default: off]
Record diagnostic-only QF_UF Ackermannization cost counters
--nelson-oppen-diagnostics [default: off]
Record diagnostic-only Nelson-Oppen interface counters
--model-equality-branching [default: off]
Enable experimental QF_UFLRA model-equality branching over shared
Real terms; not a full Nelson-Oppen model-equality implementation
--no-model-equality-mutation [default: off]
Disable the Section 5.2 greedy LRA model-diversification sweep
used by the experimental QF_UFLRA shared-model and model-equality
branching paths
--model-equality-mutation-scope TEXT:{all,care} [all]
QF_UFLRA LRA model-mutation scope: all shared Real terms or
current EUF care-pair endpoints
--nelson-oppen-prop TEXT:{exact,off,final,online} [final]
QF_UFLRA Nelson-Oppen interface equality propagation mode. Exact
keeps the mandatory convex closure but disables opportunistic LRA
producers; off is a backward-compatible alias for exact. Pure
QF_UF and QF_LRA keep their direct theory propagators
--model-equality-branch-budget UINT:INT in [0 - 1000000] [16]
Maximum QF_UFLRA model-equality branch assumptions per check-sat
--model-equality-branch-policy TEXT:{first,ranked,adaptive,care-queued} [first]
QF_UFLRA model-equality branch policy
--nelson-oppen-arrangement-probe-limit UINT:INT in [1 - 1000000000] [unlimited]
Return unknown once mixed QF_UFLRA final equality sharing or
arrangement/model reconstruction has used this many temporary LRA
consistency probes
--euf-dynamic-ackermann-shadow [default: off]
Shadow-evaluate SAT-visible dynamic Ackermann clauses without
adding them
--euf-diseq-ackermann [default: off]
Enable watched QF_UF disequality Ackermann propagation
--euf-diseq-ackermann-max-width UINT:INT in [2 - 1000] [3]
Maximum width of watched disequality Ackermann clauses
--euf-diseq-ackermann-queue-budget UINT:INT in [0 - 1000000000] [4096]
Maximum watched disequality Ackermann candidates to inspect per
propagation round
--euf-diseq-ackermann-per-symbol UINT:INT in [0 - 1000000000] [64]
Maximum watched disequality Ackermann candidates per function
symbol
--euf-prop-budget TEXT [auto]
EUF propagation candidate budget: auto, unlimited, or a
nonnegative integer
--euf-prop-delivery, --prop-delivery-budget TEXT [1000]
EUF propagation delivery budget: auto, unlimited, or a
nonnegative integer; 0 means unlimited
--finite-domain-eqdefs-auto-domain-limit UINT:INT in [0 - 1000000] [8]
Maximum finite-domain value count for auto equality definitions;
0 means unlimited
--finite-domain-eqdefs-auto-clause-limit UINT:INT in [0 - 100000000] [5000]
Maximum generated equality-definition clauses per check-sat in
auto; 0 means unlimited
--finite-domain-eqdefs-auto-term-limit UINT:INT in [0 - 100000000] [5000]
Maximum initial reachable-term count for auto equality
definitions on single-assertion formulas; 0 means unlimited
--prop-interval UINT:INT in [1 - 1000000] [32]
Online EUF propagation discovery interval
--prop-assign-threshold FLOAT:FLOAT in [0 - 1] [0.25]
Skip online EUF propagation discovery above this assigned-atom
fraction
--quantifier-instances-per-round UINT:INT in [1 - 1000000000] [128]
Quantified UF: enumerative instances queued per complete
assignment
--quantifier-stall-tuples UINT:INT in [0 - 1000000000] [65536]
Quantified UF: tuples a quantifier may visit without a new lemma
before a round that has queued lemmas hands them to SAT; 0 never
yields
--quantifier-max-instances UINT:INT in [1 - 1000000000] [100000]
Quantified UF: distinct instances generated before answering
unknown
--quantifier-tuple-order TEXT:{max,max-colex,sum,leximax,deepening,random} [sum]
Quantified UF: tuple enumeration order
--quantifier-deepening-increment UINT:INT in [1 - 1000000] [2]
Quantified UF: maximum-depth increment of the deepening tuple
order
--quantifier-random-seed UINT [0]
Quantified UF: seed of the random tuple order
--quantifier-export-pools FILE
Quantified UF: write the instantiation tuples and Skolem lemmas
as SMT-LIB pools to FILE, for scripts/quantifier_pool_check.py
Preprocessing options:
--no-extended-simplification [default: off]
Disable the ite/div/mod/abs rewrites that run before lowering
(lowering itself always runs)
--extended-simplification-rounds UINT:UINT in [0 - 64] [1]
Traversals the extended-term simplification runs; more rounds
reach deeper nested ite, at a cost that is exponential in the
limit
--ite-equality-distribution [default: on]
Distribute (= u (ite c a b)) over the branches when neither
branch is itself an ite
--no-ite-equality-distribution [default: off]
Disable (= u (ite c a b)) distribution
--cite-simplification [default: on]
Decide atoms over constant if-then-else terms branch by branch
(open-leads lead 16, piece 1)
--no-cite-simplification [default: off]
Disable constant if-then-else simplification
--arithmetic-atom-canonicalization [default: off]
Enable experimental primitive-integer canonicalization of
proportional Real comparisons and equalities before
clausification
--preprocessing-mode TEXT:{off,basic,strong,auto} [auto]
Preprocessing preset for all supported logics
--incremental-mode TEXT:{rebuild,assumptions} [rebuild]
Session engine; assumptions is opt-in for QF_LRA and QF_UF
--auto-preprocess-selector TEXT:{legacy,structural} [legacy]
Auto preprocessing selector: legacy assertion-count heuristics or
representation-stable structural analysis
--auto-preprocess-large-conjunct-limit UINT:INT in [0 - 100000000] [10000]
Maximum implicit top-level conjunct occurrences for repeated auto
preprocessing; 0 means unlimited
--preprocessing-passes, --preprocess-passes UINT:INT in [0 - 100] [4]
Number of shared preprocessing passes to run
--boolean-flatten-threshold UINT:INT in [0 - 1000000] [0]
Flatten nested and/or nodes during preprocessing up to this
arity; 0 disables
--boolean-flatten-post-threshold UINT:INT in [0 - 1000000] [2048]
Apply the same bounded And/Or flattening again AFTER the
rewriting preprocessing passes, up to this arity; 0 disables.
Those passes build fresh nodes through TermManager, which no
longer flattens at construction, so they reintroduce nesting that
--boolean-flatten-threshold (which runs before them) cannot see.
0 disables
--boolean-implies-rewrite TEXT:{off,clause,all} [off]
Post-preprocessing implication rewrite: off, clause (only expose
flat clauses), or all (rewrite A=>B to (or (not A) B) without
distribution)
--preprocessing-adaptive-extra-passes UINT:INT in [0 - 100] [4]
Additional adaptive preprocessing passes after the configured
pass cap
--preprocessing-adaptive-shrink-percent UINT:INT in [0 - 100] [10]
Minimum reachable-term shrink percentage required for another
adaptive pass
QF_LRA theory options:
--lra-propagation [default: on]
Enable QF_LRA same-slack bound propagation (Milestone 3b)
--no-lra-propagation [default: off]
Disable QF_LRA bound propagation (conflict detection only)
--lra-row-propagation [default: off]
Enable experimental QF_LRA row-based/interval bound propagation
across different variables (only takes effect if
--lra-propagation is also on)
--lra-bidirectional-row-propagation [default: off]
Enable the reverse direction of --lra-row-propagation: tighten a
row's other terms from its own bound, not just derive the row's
own implied bound (only takes effect if --lra-row-propagation is
also on)
--lra-row-propagation-max-row-size UINT:POSITIVE [64]
Cap on the row length --lra-row-propagation will derive an
implied bound for. Rows longer than this are skipped, not
truncated
--lra-row-propagation-max-fanout UINT:POSITIVE [64]
Cap on how many rows a single bound change may trigger a
--lra-row-propagation scan over. A variable occurring in more
rows than this propagates nothing that round
--lra-bidirectional-row-propagation-max-row-size UINT:POSITIVE [32]
Row-length cap for the reverse direction
(--lra-bidirectional-row-propagation). Smaller than the forward
cap because that direction costs O(row size) per other term, not
per row
--lra-bidirectional-row-propagation-max-fanout UINT:POSITIVE [32]
Fanout cap for the reverse direction
(--lra-bidirectional-row-propagation)
--lra-theory-decisions [default: off]
Enable experimental QF_LRA theory-guided decisions: the
arithmetic theory ranks candidate atoms via CaDiCaL's cb_decide
and supplies the decision literal itself instead of leaving every
decision to generic VSIDS
--lra-equality-propagation [default: off]
Enable experimental pure QF_LRA model-unit equality discovery and
propagation of existing difference comparisons (IPASIR-UP only)
--lra-model-phase [default: auto]
Enable model-based SAT phase hints (automatic for QF_LRA rebuild
queries with auto preprocessing): keep CaDiCaL's variable choice,
but refresh arithmetic atom polarity from the current tableau
assignment at quiescence points
--no-lra-model-phase [default: off]
Disable model-based SAT phase hints
--lra-pivoting-rule TEXT:{bland,dantzig,soi,sparse} [sparse]
QF_LRA Check/Pivot variable-selection rule: sparse (prices what a
pivot costs: among the entering candidates that all repair the
violation equally, take the one occurring in the fewest rows,
since those are exactly the rows the pivot rewrites), bland
(anti-cycling-proven), dantzig
(largest-violation/largest-coefficient), or soi
(Sum-of-Infeasibilities Simplex, King/Barrett/Dutertre FMCAD 2013
-- a global Check/Pivot objective across every violated row at
once). All but bland fall back to bland selection after enough
pivots within one check(), which is what keeps termination proven
--lra-least-violated-leaving [default: off]
Experimental leaving-variable rule from Griggio's thesis (2.5.3,
p.53):
pick the LEAST-violated basic variable, tie-broken by the shorter
row.
Only meaningful under --lra-pivoting-rule sparse
--no-lra-sparse-leaving [default: off]
Disable the leaving-side half of --lra-pivoting-rule sparse
(prefer repairing a violated variable whose row is short, using
violation magnitude only as a tie-break), for ablation
--lra-sparse-pricing-candidates UINT:INT in [0 - 1000000] [16]
How many eligible entering candidates --lra-pivoting-rule sparse
scores before taking the best seen so far (0 means score every
eligible candidate). 1 is the cheapest possible pricing. Never
cuts short the search for whether an eligible candidate exists,
so any value is sound
--lra-soi-minimize TEXT:{quickxplain,deletion,none} [quickxplain]
How --lra-pivoting-rule soi shrinks a multi-row conflict before
turning it into a clause: quickxplain (Junker 2001), deletion
(iterative, and steerable by --lra-soi-minimize-order), or none
(ablation baseline). Inert under every other pivoting rule.
Measured, the error set averages 2.83 variables and never
exceeded 9, so this changes which minimal conflict is learned
rather than how fast it is found
--lra-soi-minimize-order TEXT:{id,row-support,violation} [id]
Order --lra-soi-minimize deletion offers candidates for removal,
worst first: id (ascending, reproduces quickxplain's input
order), row-support (longest row first -- the row support
dominates clause length, so this sheds the rows contributing most
literals), or violation (largest bound violation first)
--lra-bland-fallback-factor UINT:INT in [0 - 1000000] [4]
Per-variable coefficient of check()'s Bland's-rule fallback
point, which is factor * variables + offset pivots within one
check. Smaller switches to Bland's rule sooner: slower but
anti-cycling-proven
--lra-bland-fallback-offset UINT:INT in [0 - 1000000000] [64]
Constant term of the Bland's-rule fallback point
--mixed-dispatch TEXT:{narrow,wide} [narrow]
Which formulas reach the mixed EUF/LRA solver: narrow (only a
Bool-sorted function APPLICATION counts as an EUF predicate, so a
formula that is pure QF_LRA apart from propositional variables
stays on the pure path) or wide (a Bool-sorted constant counts
too -- the pre-2026-08-07 behaviour, routing any QF_LRA formula
containing one propositional variable to the mixed solver).
Usually much worse, but genuinely better on some instances; kept
as a portfolio dimension and so differential fuzzing can reach
the mixed path
--lra-fixed-elimination [default: off]
Pivot a basic LRA variable out of the basis as soon as its bounds
coincide (heuristics item H7). It nets to nothing on the
scrambled competition set, but doubles the >5MB band, so it is
worth enabling on equality-dominated input
--no-qf-uflra-fixed-elimination [default: off]
Disable mixed QF_UFLRA fixed-variable elimination, which exposes
EqRow interface equalities before the exact pair fallback
--gaussian-elimination [default: on]
Enable QF_LRA Gauss-Jordan elimination over asserted linear
equality systems, feeding solve-eqs (campaign-fuzzed 2026-07-25)
--no-gaussian-elimination [default: off]
Disable QF_LRA Gauss-Jordan equality-system elimination
--qf-uflra-candidate-final-scan [default: off]
Enable experimental mixed QF_UFLRA candidate-first final LRA
equality scans before falling back to the full shared-Real pair
scan
--qf-uflra-lra-equality-producer TEXT:{legacy,model-unit,adaptive} [legacy]
LRA-to-EUF opportunistic equality producer: legacy exact-offset
row indexes or model-unit current-model-filtered unit rows;
adaptive bootstraps legacy to a propagation fixed point, then
uses model-unit until a later shared-model split
--qf-uflra-model-reconciliation [default: on]
Explicitly enable convex QF_UFLRA shared-model reconciliation
with scratch LRA mutation, EUF compatibility checks, and lazy
positive equality splits
--no-qf-uflra-model-reconciliation [default: off]
Disable convex QF_UFLRA shared-model reconciliation and use the
explained exact equality-sharing fallback
--monotone-elimination [default: auto]
Enable monotone (one-sided) real-variable elimination (automatic
for
QF_LRA rebuild queries with auto preprocessing): a
variable every constraint pushes the same way is discharged and
its
atoms folded to constants, shrinking the Boolean structure.
Models are
reconstructed for eliminated variables
--no-monotone-elimination [default: off]
Disable monotone real-variable elimination
--guarded-real-equality-lowering [default: off]
Enable experimental guarded Real equality lowering: rewrite a
disjunction with one Real equality child directly to two guarded
inequalities, avoiding one Tseitin layer on some QF_LRA encodings
QF_LIA theory options:
--qf-uflia-model-combination, --experimental-qf-uflia-model-combination [default: on]
Guide non-convex QF_UFLIA arrangement search with component
models before complete fallback
--no-qf-uflia-model-combination [default: off]
Disable QF_UFLIA model guidance and start from the complete
arrangement
--qf-uflia-online-components, --experimental-qf-uflia-online-components [default: on]
Reuse trail-synchronized EUF and rational-arithmetic state during
QF_UFLIA SAT search
--no-qf-uflia-online-components [default: off]
Disable trail-synchronized QF_UFLIA components
--qf-uflia-model-decision-budget UINT [512]
Maximum QF_UFLIA model-choice batches before complete arrangement
fallback
--lia-branch-limit UINT:INT in [1 - 100000000] [100000]
QF_LIA branch-and-bound node cap: plain branch-and-bound alone
has no completeness argument (an unbounded integer-infeasible
polytope can branch forever), so once this many nodes have been
explored the search reports Unknown instead of continuing
--lia-gomory-cut-limit UINT:INT in [0 - 100000000] [100]
QF_LIA Gomory-cut round cap, run before branch-and-bound on every
candidate model: caps how many cut-and-recheck rounds are
attempted before falling through to branch-and-bound regardless
--lia-patch-limit UINT:INT in [0 - 100000000] [100]
QF_LIA patching budget, run before the integer refutation stages
on every candidate model: caps how many nonbasic moves are taken
to nudge Int variables onto integer values. 0 disables patching
--no-lia-conflict-generalization [default: off]
Disable QF_LIA conflict generalization: build each
integer-infeasibility lemma from every arithmetic atom in the
problem instead of from the GCD/cut/branch derivation that
actually proved it. The coarse form excludes one Boolean
assignment per round
SAT and DPLL(T) options:
--qf-uflra-online-euf [default: off]
Enable experimental incremental EUF callbacks and live
final-model closure reuse in mixed QF_UFLRA solving
--top-level-or-tseitin [default: off]
Always encode top-level disjunctions with Tseitin support clauses
--no-top-level-or-tseitin [default: off]
Never encode them: keep each top-level disjunction as one clause,
and turn the automatic rule off too
--no-auto-top-level-or-tseitin [default: off]
Disable the automatic rule, which encodes Tseitin-style only on
finite-domain problems having 1000-2500 top-level OR nodes and at
most 700 negations
--pure-theory-filter TEXT:{auto,on,off} [auto]
T-pure theory literal filtering mode
--theory-phase TEXT:{negative,positive,none,polarity,auto} [negative]
Initial SAT phase for theory atoms
--max-theory-conflicts UINT:INT in [1 - 1000000000] [unlimited]
Return unknown after at least this many learned theory conflicts
--cadical-option TEXT
Set a CaDiCaL integer option as name=value; may be repeated