On 11 April 2013 16:52, Pablo González de Aledo <[email protected]> wrote: > Hi Dan. Thanks for your help and quick answer :-). > > Although STP solver only works with bitvectors, I think now it exists > more advanced solvers like z3 that support more logics. About the > disadvantages of using bitvectors, my humble opinion is that, even if > they have enough expressive power to represent any type on a computer, > they represent it in the 'most general way'. Disadvantages in such > generality might be speed ( I believe integer solvers are faster than > bit-vector ones ), or larger queries.
Z3 does support more SMT-LIBv2 logics than STP but the SMT-LIBv2 logics that use integers are "mathematical" integers rather than "bitvector" integers. Using "mathematical" integers in place of "bitvector" integers would be imprecise (e.g. miss bugs related to integer overflow and underflow). It would be interesting to know if it's faster though. > I'm currently starting a PhD in verification. Do you (for all) think > integrating an integer --or real-- solver in klee would be an > interesting subject?. I think modelling floating point numbers as reals could be interesting. Currently KLEE does not support symbolic floating point numbers so adding support for floating point numbers although imprecise is certainly better than no floating point support at all. Regards, Dan. _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
