[klee-dev] Path Search Heuristics

2015-05-24 Thread Zhiyi Zhang
Hi all, I have some questions about path search heuristics used in KLEE. 1, It seems that KLEE can NOT generate test cases when I only used search==nurs:covnew as the path search heuristic. Moreover, when using search==nurs:md2u, search==nurs:icnt, search==nurs:cpicnt or search==nurs:qc as as

Re: [klee-dev] Path Search Heuristics

2015-05-24 Thread Zhiyi Zhang
Hi Bartell, Thanks for your reply very much. 1, KLEE keeps running without printing anything. I set KLEE running time for one hour, but it stops very quickly. There is no error reports. In the klee-out folder, there are only assembly.ll and run.stats files. However, when I used bfs, dfs, random

[klee-dev] STP-Make copy of solver object

2015-05-24 Thread Saksham Jain
Hi, This question is not strictly wrt to KLEE. I am trying to make my own symbolic executioner in python. I am using STP for this. The issue I am facing is wrt to making an independent copy of STP solver. During symbolic execution, whenever my program encounter a branch, I try to make a duplicate