Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-12-02 | Implement :named and let abbreviation modes in ExprSMTLIBPrinter | Raimondas Sasnauskas | |
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET) * Remove the now defunct ExprSMTLIBLetPrinter * Improve performance of ExprSMTLIBPrinter::scan() by keeping track of visited Expr to avoid visiting them again * Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr() | |||
2014-04-02 | Modify the SMT-LIB printer to declare arrays in a deterministic ↵ | Peter Collingbourne | |
(alphabetical) order. | |||
2012-10-24 | Patch by Dan Liew: "Added primitive test that checks kleaver's new | Cristian Cadar | |
-print-smt option. Improved Feature/ExprLogging.c test: - Now (primitive) checks the result of -write-smt2s - Now (primitive) checks the result of -write-pcs - Now (primitive) checks the result of -write-cvcs" git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166569 91177308-0d34-0410-b5e6-96231b3b80d8 |