projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b3ec697) | patch
Tighten policy for unsat cores in sygus core connective (#7911)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 11 Jan 2022 15:10:41 +0000 (09:10 -0600)
committerGitHub <noreply@github.com>
Tue, 11 Jan 2022 15:10:41 +0000 (15:10 +0000)
commit0a14d681c473ac77575e6191e7a2c274fd32b755
tree5584e03a90fa2992a6119fb8d5c844ad9d988002tree
parentb3ec6979e39ea329e45c4158f51680fdd5858781commit | diff
Tighten policy for unsat cores in sygus core connective (#7911)

Previous policy was due to limitations on options on subsolvers, which no longer exist.

Fixes cvc5/cvc5-projects#354.
Fixes #7902.
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers/sygus/cegis_core_connective.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/issue7902-abd-subsolver-uc.smt2 [new file with mode: 0644] blob