Model Validation feeback

[bobot]

No description provided.

[bobot]

@Gbury You can be interested in taking a look at this little model verification summary. also @martinjonas @mbromber

[Gbury]

Very interesting.

The ite problem can be resolved fairly easily (actually, I think it should already be lazy, because you need that for recursive fonctions, but I may misremember), but as you point out, similar problems may arise with implications, and maybe other functions in the future, so I think we need some kind of specification in the standard of which functions are expected to be evaluated lazily.

Hopefully, with the new printing capabilities of Dolmen, I'll try to "fix" the problems in the SMT-LIB that do not respect the standard, so that new year it can be fully compliant (fingers crossed, ^^).