Looking for linear constraints solvers are slow on

[Andrea Aquino]

Dear all,

I am Andrea Aquino, a Ph.D. student at Università della Svizzera Italiana (Lugano, Switzerland).
I am currently working with my colleague Meixian Chen on a sort of cache for linear constraints extracted by programs by symbolic execution.

We are currently looking for linear formulae extracted from real programs which take a lot of time to be solved either with Z3, Yices or any other solver.

Can you give us any advice on how to find some? Do you have some constraints of this kind we could analyze?

Best regards,
Andrea Aquino, Meixian Chen

[Hristina Palikareva]

Hi Andrea,

Which logic are you after? Also, what input format do you need? We have
QF_ABV benchmarks in SMT2 format, if you are interested. They are all
extracted from running KLEE on real-world software, e.g. GNU Coreutils.

Best regards,
Hristina

Post by Andrea Aquino
Dear all,
I am Andrea Aquino, a Ph.D. student at Università della Svizzera Italiana (Lugano, Switzerland).
I am currently working with my colleague Meixian Chen on a sort of cache for linear constraints extracted by programs by symbolic execution.
We are currently looking for linear formulae extracted from real programs which take a lot of time to be solved either with Z3, Yices or any other solver.
Can you give us any advice on how to find some? Do you have some constraints of this kind we could analyze?
Best regards,
Andrea Aquino, Meixian Chen
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev