This PR fixes a bug in D_cnf that have been exposed by #1130. Before merging Enum into ADT the situation was as follows:
simple ADT with several constructors and with at least one payload was sent to the Adt theory
simple ADT with several constructors but no payload was sent to Enum theory
simple ADT with a single constructor was sent to the Record theory.
The last corner case includes a corner corner case: an ADT with a single constructor without payload (so basically the unit type with an extra step...)
The D_cnf included a bug. It produced single constructors without payload of type ADT instead of type record but the check done in is_mine_symb prevented from sending it to Adt. As I removed this check, we got an assert on the following input:
(set-logic ALL)
(declare-datatype t ((Record)))
(define-fun a () t Record)
(check-sat)
After this patch, the situation is as follows:
simple ADT with several constructors is sent to the Adt theory
simple ADT with only one constructor is sent to the Record theory
mutually recursive ADT whose all the types are record is sent to the Record theory
This PR fixes a bug in
D_cnf
that have been exposed by #1130. Before mergingEnum
intoADT
the situation was as follows:Adt
theoryEnum
theoryRecord
theory.The last corner case includes a corner corner case: an ADT with a single constructor without payload (so basically the unit type with an extra step...)
The
D_cnf
included a bug. It produced single constructors without payload of type ADT instead of type record but the check done inis_mine_symb
prevented from sending it toAdt
. As I removed this check, we got an assert on the following input:After this patch, the situation is as follows:
Adt
theoryRecord
theoryRecord
theory