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 > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
