summaryrefslogtreecommitdiff
path: root/src/options/quantifiers_options
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/quantifiers_options')
-rw-r--r--src/options/quantifiers_options2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 34f399f45..227540f45 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -258,7 +258,7 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode
template mode for sygus invariant synthesis
-option sygusDirectEval --sygus-direct-eval bool :default false
+option sygusDirectEval --sygus-direct-eval bool :default true
direct unfolding of evaluation functions
# approach applied to general quantified formulas
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback