Exploit the match construct of SMTLIB 2.6
The match
construct for ADTs has been introduced in SMTLIB 2.6 but the smtv2 printer does not use it, and uses instead nested ite
expression and binders.
I would be better to use the match
construct.
Prochaines maintenances programmées: lundi 06/05, lundi 03/06, lundi 01/07
Pour plus d'informations: https://doc-si.inria.fr/display/SU/Gitlab
The match
construct for ADTs has been introduced in SMTLIB 2.6 but the smtv2 printer does not use it, and uses instead nested ite
expression and binders.
I would be better to use the match
construct.