diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-03-09 11:40:59 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-09 11:40:59 -0800 |
| commit | c6085d9b70beb9a2be5a26a3c085b4f1a1758410 (patch) | |
| tree | 71f9fc4d9df2264994f34dabf77fd16de90ea851 /src/options/smt_options | |
| parent | 6330388f2606e82c4348de9ba6c62c4de7861cd9 (diff) | |
Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)
Diffstat (limited to 'src/options/smt_options')
| -rw-r--r-- | src/options/smt_options | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/options/smt_options b/src/options/smt_options index 72189ea13..811cc5a71 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -54,6 +54,9 @@ option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-uns option dumpUnsatCoresFull dump-unsat-cores-full --dump-unsat-cores-full bool :default false :link --dump-unsat-cores :link-smt dump-unsat-cores :notify notifyBeforeSearch dump the full unsat core, including unlabeled assertions +option unsatAssumptions produce-unsat-assumptions --produce-unsat-assumptions bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate proofEnabledBuild :notify notifyBeforeSearch + turn on unsat assumptions generation + option checkSynthSol --check-synth-sol bool :default false checks whether produced solutions to functions-to-synthesize satisfy the conjecture |