diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-30 14:13:47 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-30 20:13:47 +0000 |
| commit | 641c531bcb9df45ca6c19f3f9ccfad08afbe17de (patch) | |
| tree | aa81b2a9a0eea2376642416264439a636b3670d0 /src/proof/proof_generator.h | |
| parent | c5f96858234d6634b744ef8e4250316c62196430 (diff) | |
Proper check for first-class types in datatype subfields (#7712)
Fixes two issues with our check for datatype subfields (isFunctionLike -> isFirstClass): functions should be allowed, RegLan should not.
Fixes cvc5/cvc5-projects#368. That issue now throws an error:
(error "Parse Error: proj-368.smt2:3.39: cannot use fields in datatypes that are not first class types
(declare-datatype x ((_x (x8 RegLan))))
^
")
This adds a regression showing we allow functions as subfields.
Diffstat (limited to 'src/proof/proof_generator.h')
0 files changed, 0 insertions, 0 deletions