projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c9daef3) | patch
Ensure configuration of shared selectors is consistent in SyGuS subsolver (#7927)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 12 Jan 2022 21:46:38 +0000 (15:46 -0600)
committerGitHub <noreply@github.com>
Wed, 12 Jan 2022 21:46:38 +0000 (21:46 +0000)
commitffbdd1b3c3352fa342683facb44ca3e916844ac7
tree02ff484806010b0e39d4034e9e9aa52a4ae718cetree
parentc9daef3594dec48693ede0c13e7fc9804835ef14commit | diff
Ensure configuration of shared selectors is consistent in SyGuS subsolver (#7927)

This prevents the SyGuS subsolver from having a different configuration of dt-share-sel than the main SyGuS solver. Having this mismatch can lead to incorrect synthesis results.

Fixes #7925.
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_verify.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/issue7925-dt-share-config.sy [new file with mode: 0644] blob