[klee-dev] Looking for linear constraints solvers are slow on

[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


On 25/06/14 16:05, Andrea Aquino wrote:
> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>