[klee-dev] Why restrict to bitvectors?

[Daniel Liew]

On 11 April 2013 16:52, Pablo González de Aledo <pabloga at teisa.unican.es> 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.