projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3c4ad6a) | patch
Fixes related to set defaults for sygus/proofs (#8395)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 25 Mar 2022 17:02:23 +0000 (12:02 -0500)
committerGitHub <noreply@github.com>
Fri, 25 Mar 2022 17:02:23 +0000 (14:02 -0300)
commitb3ba5a8eca70539ac00719eb3de68cb214033c59
tree08c4d1ca8d618ffe4821d154e521ede31a1e630ctree
parent3c4ad6a462ea1f583950af993468a10d45ca7e0ccommit | diff
Fixes related to set defaults for sygus/proofs (#8395)

This ensures we always report that SyGuS is incompatible with proofs. As a result, we require disabling sygus in 2 contexts where it should have been disabled before.
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers/query_generator_unsat.cpp diff | blob | history
src/theory/quantifiers/sygus/cegis_core_connective.cpp diff | blob | history