Feature: Random_seed parameter

[tiferrei]

Hi there,

Thanks a lot for this project! I just added a parameter for fixing the random seed (for Z3), and thought I'd submit a PR to upstream if anyone else is interested.

I had to remove the %%VERSION%% template from main.ml, as it was giving me compilation issues. AFAIK this seems to not be populated at any point, but I am happy to remove that commit.

Thanks,

Tiago

[filipeom]

Thank you so much your contribution! Everything looks good to me. Let me know if you have any issues using smtml!

[tiferrei]

Thanks a lot for getting this merged so quickly!

Now that you mention it, I have had some issues getting the cvc5 lib installed through nix (nix build 'github:tweag/opam-nix#cvc5.latest'), probably something to do with the static libraries and macOS, however this seems to be a Nix specific problem.

Additionally, I noticed that there is no support for tuples or enums, which at first gave me some issues but I was able to work around with lists and some hacky integer representations. Thanks again!

[filipeom]

Now that you mention it, I have had some issues getting the `cvc5` lib installed through nix (`nix build 'github:tweag/opam-nix#cvc5.latest'`), probably something to do with the static libraries and macOS, however this seems to be a Nix specific problem.

Yeah, unfortunately, we don't have a lot of time to work on the cvc5 bindings. Because of this, the work to make the cvc5 library dynamically linkable is somewhat stalled (formalsec/ocaml-cvc5#38).

Additionally, I noticed that there is no support for tuples or enums, which at first gave me some issues but I was able to work around with lists and some hacky integer representations.

For enums, we already have the mappings for them in smtml (https://github.com/formalsec/smtml/blob/990331cda5b88278355a8325044c9ac6fdecba0d/src/smtml/mappings_intf.ml#L697), but they are not yet integrated into the `Expr` module. We will eventually add support, but I can't give you a timeline.

[tiferrei]

For enums, we already have the mappings for them in smtml

Ah very nice! No worries, it is not a key feature for me

[filipeom]

These changes should be included in smtml.0.15.0 if you're interested. Should be available in Opam once ocaml/opam-repository#28957 is merged.