search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

Support timelimit on Windows #1201

Open Halbaroth opened 1 month ago

Halbaroth commented 1 month ago

We do not support timelimit and :reproducible-resource-limit on Windows because our implementation relies on Unix signals. We should support them using GC alarms as it does in Dolmen.

bclement-ocp commented 1 month ago

Note: we should use step bounds for reproducible-resource-limit (but we don't support per-goal step bounds at the moment). As per the SMT-LIB specification it must be guaranteed that running the same code on the same machine with the same reproducible-resource-limit give the same result, so using real time does not actually implement the specification (it is not reproducible).