projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9a58e63) | patch
Datatypes lemmas: share only external types (#5997)
authoryoni206 <yoni206@users.noreply.github.com>
Thu, 25 Feb 2021 20:36:05 +0000 (12:36 -0800)
committerGitHub <noreply@github.com>
Thu, 25 Feb 2021 20:36:05 +0000 (14:36 -0600)
commit6a4b16c643d71c9318042ba7b9d42af71c58ac2f
tree0092464e48a09bd71eff04b1d4d44cc3fac31bc0tree
parent9a58e63237298be0c81fe88096f65d935be97e82commit | diff
Datatypes lemmas: share only external types (#5997)

Forcing lemmas in datatypes used to be done only for external types.
This was changed to consider all types, which is not needed.
This PR brings back the restriction to external types.
src/theory/datatypes/theory_datatypes.cpp diff | blob | history