projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2160fef) | patch
Option exception when incompatible with proofs (#8064)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 23 Feb 2022 18:46:02 +0000 (12:46 -0600)
committerGitHub <noreply@github.com>
Wed, 23 Feb 2022 18:46:02 +0000 (18:46 +0000)
commit4cf79c69a6c6ef8bb26f0119e85450a3cf7028a3
tree7163459e5452ccad75d2dd47f5cfd69ba5c2da74tree
parent2160fef57b24ef35d9334f5bb5faa1ba87c8a2f4commit | diff
Option exception when incompatible with proofs (#8064)

This changes set defaults so that it doesn't silently disable proofs or unsat cores.

Fixes cvc5/cvc5-projects#440.
12 files changed:
src/smt/set_defaults.cpp diff | blob | history
test/regress/regress0/quantifiers/lra-triv-gn.smt2 diff | blob | history
test/regress/regress1/issue3970-nl-ext-purify.smt2 diff | blob | history
test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 diff | blob | history
test/regress/regress1/sygus/issue3201.smt2 diff | blob | history
test/regress/regress1/sygus/issue3247.smt2 diff | blob | history
test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 diff | blob | history
test/regress/regress1/sygus/issue4009-qep.smt2 diff | blob | history
test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 diff | blob | history
test/regress/regress1/sygus/issue4083-var-shadow.smt2 diff | blob | history
test/regress/regress1/sygus/proj-issue185.smt2 diff | blob | history
test/unit/api/cpp/solver_black.cpp diff | blob | history