yoni206

The link https://github.com/pysmt/pysmt/tree/issue_187_enum_support is invalid. Does the branch still exist? and if so, could you please provide a current link to it? Thanks

Well, ultimate goal is to support the theory of datatypes (smtlib 2.6). An intermediate goal would be to support datatypes with null-ary constructors (enums).

Thank's for the link! I am not using `match` currently. AFAIK, cvc4 and z3 support it (at least, i can run some benchmarks on both).

Maybe these examples can be useful? https://github.com/CVC4/CVC4/tree/master/test/regress/regress0/datatypes

Excuse me for popping out of nowhere here, but I would just like to say that I would love to have integer modulo operator in pysmt! If mod is simpler...

I have installed vim.gnome-py2, which has both python and clientserver support. Also, I ran update-alternatives for both vim and gvim. Is there a way to get Yavide work through vim...

If this is still on the table then +1 -- it would be great to see percentage on the reports.