projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: eb3b043) | patch
Ensure match terms are exhaustive in its type rule (#7807)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 15 Dec 2021 23:49:19 +0000 (17:49 -0600)
committerGitHub <noreply@github.com>
Wed, 15 Dec 2021 23:49:19 +0000 (23:49 +0000)
commit4a7c0c73f69aabb20be4c79c47047ce23d3358b0
treed56657f559704e22ed683d75e1eb526b1753b8a6tree
parenteb3b04319a26e3573dd2ba520f12432ce2d797b3commit | diff
Ensure match terms are exhaustive in its type rule (#7807)

Fixes cvc5/cvc5-projects#382.

Makes it so that we always fully type check match terms before they are rewritten, which guards potential unsoundness.
src/theory/datatypes/datatypes_rewriter.cpp diff | blob | history
src/theory/datatypes/theory_datatypes_type_rules.cpp diff | blob | history
test/unit/api/cpp/solver_black.cpp diff | blob | history