Hi all, I've just pushed several patches by Dan Liew (thanks, Dan!) which add to KLEE the ability to output queries in the standard SMT-LIB language (see http://www.smtlib.org/ for more info on SMT-LIB). This makes it easy to debug queries outside KLEE, and to quickly see how other SMT solvers compare to STP.
In particular, there are now several new options, --write-smt2s, --use-query-log=all:smt2, etc., which can be used to output queries in the SMT-LIBv2 format; these options are documented at http://klee.llvm.org/klee-files.html. Best, Cristian _______________________________________________ klee-dev mailing list klee-dev@keeda.stanford.edu http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
