diff options
author | Peter Collingbourne <pcc@google.com> | 2014-04-30 22:57:08 -0700 |
---|---|---|
committer | Peter Collingbourne <pcc@google.com> | 2014-05-11 15:50:10 -0700 |
commit | abd13a505e64b061a53b6c0562fa74857aba6104 (patch) | |
tree | e7951ee650645b1a0c7aed4afa09f371db90de7f /lib/Core/ExternalDispatcher.cpp | |
parent | d10513097420196493b4a408c6cf75cbd53b8351 (diff) | |
download | klee-abd13a505e64b061a53b6c0562fa74857aba6104.tar.gz |
Fix the logic in ExprSMTLIBPrinter::getSort
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.
Diffstat (limited to 'lib/Core/ExternalDispatcher.cpp')
0 files changed, 0 insertions, 0 deletions