-
Sylvain Dailler authored
This commit solves a CVC4 limitation on boolean inside datatypes for CE. It converts them to bv by adding a new printer. This commit is a hack and it will be reverted when the bug is solved in CVC4. * Makefile.in (Makefile): Added new printer. * drivers/smtv-libv2_cvc_ce.drv: (printer): new printer used is smtv2_cvc_ce * src/driver/parse_smtv2_model_lexer.mll (parse): Changed the way constructor of datatype are detected. * src/printer/smtv2_cvc_ce.ml (print_constructors): Projections to bool are changed to projections to bitvectors. Duplicate projections are generated which returns bool and are used in the rest of smtv2 generated. Change-Id: Ib2eba92aa788938b0bec30f8c156e9b235896881
a303ae72