summaryrefslogtreecommitdiff
path: root/src/options/smt_options
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/smt_options')
-rw-r--r--src/options/smt_options4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/options/smt_options b/src/options/smt_options
index c701d5c20..fa6c3ae4e 100644
--- a/src/options/smt_options
+++ b/src/options/smt_options
@@ -40,7 +40,9 @@ option dumpProofs --dump-proofs bool :default false :link --proof :link-smt prod
option dumpInstantiations --dump-instantiations bool :default false
output instantiations of quantified formulas after every UNSAT/VALID response
option sygusOut --sygus-out=MODE SygusSolutionOutMode :default SYGUS_SOL_OUT_STATUS_AND_DEF :include "options/sygus_out_mode.h" :handler stringToSygusSolutionOutMode :read-write
- output mode for sygus
+ output mode for sygus
+option sygusPrintCallbacks --sygus-print-callbacks bool :default true
+ use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)
option dumpSynth --dump-synth bool :read-write :default false
output solution for synthesis conjectures after every UNSAT/VALID response
option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback