[klee-dev] The format of generated smt files

[Zhongqiu Gao]

Hi,
I am trying to use 
--write-smt2s 
to write the path constraints into smt files. But all of the variables are defined as an array of bit vector. Is there a way to let klee specify the variable type when generating the smt files?
For example, in the source file, if x is declared as an integer, then in the smt file, it should also be defined as an integer, not an array of bit vector.
I am trying to let the solver read the smt files and generate a value, and sometimes the values it generate are overflowed. For example, we want y - 2x == 0, and it turns out
y = 131068 and x = 2147549180.
y - x - x  = -4294967296. It's not zero, but is considered 0 by the solver because 4294967296 is
1 00000000 00000000 00000000 0000000
as binary and "1" is eliminated due to overflow.


Thanks,
Zhongqiu Gao
-------------- next part --------------
HTML attachment scrubbed and removed