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