projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fb2a0d9) | patch
Fixes for corner case of decision tree learning with different types (#4887)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 13 Aug 2020 19:15:17 +0000 (14:15 -0500)
committerGitHub <noreply@github.com>
Thu, 13 Aug 2020 19:15:17 +0000 (14:15 -0500)
commitddf6526f9f3ac2410849fbf8ebf0eac09ff2a28a
treefa6355c317248c1e8ac1601f98533fb1d95c4f6btree
parentfb2a0d9aa09aa21f465aa8d62eab8492610052c3commit | diff
Fixes for corner case of decision tree learning with different types (#4887)

There was a last minute change was a typo when merging 103b5ea .
Also the fix in that commit needed to be slightly more robust to the case when either branch of an ITE had a different sygus type.

Fixes regress1.
src/theory/quantifiers/sygus/sygus_unif_io.cpp diff | blob | history