SRI-CSL / yices2

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

yices_incref_term: segmentation fault #384

Closed ptr1120 closed 2 years ago

ptr1120 commented 2 years ago

Hello,

I need to use the reference counting mechanism in order to implement proper garbage collection. As I understand I have to count every reference to a term, so for every variable (e.g. bool a) and for every operator combination of variables (e.g. a AND b). Doing so I am experiencing a segmentation fault for bigger models. I created an example that reproducible causes this segmentation fault for more than 2000 reference counted variables:

type_t bool_type = yices_bool_type();
for (int i = 0; i < 2500; ++i) {
    term_t t = yices_new_uninterpreted_term(bool_type);
    yices_incref_term(t);
}

Am I doing anything wrong?

Best regards Peter

BrunoDutertre commented 2 years ago

That was a bug in Yices. It's fixed in 43e885187140c7e400230be7e4327666babfa274.

ptr1120 commented 2 years ago

Thank you very much, it is fixed!