Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-05-11 | Fix the logic in ExprSMTLIBPrinter::getSort | Peter Collingbourne | |
This now corresponds to the sorts of the operations we emit, as far as I can tell. Read is one example of an operation that now works correctly (with 1-bit array ranges). It's also possible (but not very useful, and I don't think KLEE can produce it) for other operations such as Add to operate on 1-bit values, and this patch also fixes those. | |||
2014-04-02 | Modify the SMT-LIB printer to declare arrays in a deterministic ↵ | Peter Collingbourne | |
(alphabetical) order. | |||
2014-03-09 | Use clang-format to reformat SMT-LIB printer in LLVM style. | Peter Collingbourne | |
2013-05-08 | Patch by Dan Liew: "Renamed ExprSMTLIBPrinter method mangleQuery() to ↵ | Cristian Cadar | |
negateQueryExpression() to make it clear what it does." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@181445 91177308-0d34-0410-b5e6-96231b3b80d8 | |||
2012-10-24 | Nice patch by Dan Liew that adds support for printing queries in the | Cristian Cadar | |
SMTLIB format (part of his MSc project work). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166556 91177308-0d34-0410-b5e6-96231b3b80d8 |