search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

Deterministic time limit #129

Open alph6 opened 5 years ago

alph6 commented 5 years ago

Hi, I would like to know is there a way (or any plans for adding such) to set deterministic execution limit for Yices like Z3's "rlimit" does. In other words, to guarantee that Yices will produce the same answer for the formula on different executions or different machines.

BrunoDutertre commented 5 years ago

That should be feasible, but it will take some time.