[klee-dev] Why restrict to bitvectors?

Pablo González de Aledo pabloga at teisa.unican.es
Thu Apr 11 14:57:48 BST 2013


Hi, I'm introducing myself into klee, and I'm wondering why does klee 
restrict queries and transforms all them into bitvectors?. Wouldn't it 
be faster and easier to keep integer expressions as is, and transform 
only what is necessary because of bitwise operations such as &.|,^ ...?

Thanks




More information about the klee-dev mailing list