Daniel Dunbar wrote: > Well, it's certainly possible that you are getting a query that is > hard to solve. It's NP-hard, after all, so it doesn't take much work > to find queries that will take days to solve. > > That said, if it only happens on one machine maybe something else is > going on. What versions of gcc do the machines have? Maybe MINISAT is > being miscompiled?
cluestick has gcc (GCC) 4.3.0 20080428 (Red Hat 4.3.0-8), bohr has gcc (Debian 4.3.4-5) 4.3.4. I don't think any of these are outdated enough to be suspected, but how can I tell if one is causing the proble? By the way, the Makefile is certainly broken -- running make from $KLEE_ROOT doesn't recognize any changes in the source files in $KLEE_ROOT/stp/AST, nor does running make from $KLEE_ROOT/stp. Either you have to run "make clean" each time, or after changing any source file you have to do "make" first in $KLEE_ROOT/stp/AST, then in $KLEE_ROOT/stp, and then in $KLEE_ROOT. > > Otherwise it might be worth sending the query to Vijay, he may have a > better idea. I attached a query (printed from KLEE) that I saw more than once that caused the indefinite loop. How can I feed this into the stand-alone STP solver ($KLEE_ROOT/stp/bin/stp, I guess)? It seems to expect a certain grammar that $KLEE_ROOT/stp/bin/stp doesn't accept directly. And how can I reach Vijay? (Are you on this list? :D) -- Seungbeom Kim -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: query_example.txt Url: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20091015/7abc5bff/attachment.txt
