[klee-dev] question about concolic execution using klee

[xiaoqixue_1]

Hi, all
 
I used klee’s seed-mode and zesti to test in concolic mode. I thought it would execute the program and keep the path constraints with solving them. Because the seeds could tell which branch would be taken.
But klee and zesti took much time to evaluate or solve conditions when I did some test whose symbolic input greater than 100 bytes.
 
The test commands as follows:
klee --libc=uclibc --posix-runtime -libz --start-debug-inst=0 --dump-func-trace --check-div-zero=false --check-overshift=false -xlib --lib-path=/home/xqx/test/libpng-test/libpng-1.2.4/libpng.bca --seed-out=/tmp/seed208.ktest -only-seed -named-seed-matching /home/xq    x/test/libpng-test/test-libpng124/pngtest.bc /tmp/1.png --xqx-sym-file /tmp/1.png 0 104 2  
(--xqx-sym-file to specify the symbolic file and data)
Zesti-klee --zest --use-symbex=1 --symbex-for=10 --search=zest --zest-search-heuristic=br --zest-continue-after-error=true --libc=uclibc --posix-runtime -libz -emit-all-errors /home/xqx/test/libpng-test/test-libpng124/pngtest.bc /tmp/basn0g02.png
 
I used klee to run “pngtest.bc /tmp/basn0g02.png”, it could complete in 68s, However, It could not run over when I use klee seed-mode or zesti in 20 hours.
 
And I think it need not to solve the constraints when we have a seed. I have search the mail-list for the related discussions, but none has an answer.
The related discussions as follows:
https://mailman.ic.ac.uk/mailman/htdig/klee-dev/2013-November/000488.html
https://mailman.ic.ac.uk/mailman/htdig/klee-dev/2013-November/000489.html
https://www.mail-archive.com/klee-dev%40imperial.ac.uk/msg00680.html
 
Did I run klee or zesti in wrong command?
Could you give me some solution?

Best Regards
xqx