diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-04-10 09:49:04 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-04-15 21:08:38 +0100 |
| commit | 1a175c67402430c8e6a970d42660dcf3b23110aa (patch) | |
| tree | 9001b1ac943bf1e45a24a0620e87bcafc1c08f24 /test/Feature/MultiMkSym.c | |
| parent | 44cceb1eb7ab58b153a20d12c84d6b0b352e05da (diff) | |
| download | klee-1a175c67402430c8e6a970d42660dcf3b23110aa.tar.gz | |
Fix the handling of AShrExpr in ExprSMTLIBPrinter so that an overshift
always goes to zero (matches LLVM's APInt::ashr(...)). This is meant to partially address issue #218. There are a few problems with this commit * It is possible for AShrExpr to not be abbreviated because the scan methods will not see that we print the 0th child of the AShrExpr twice * The added test case should really be run through an SMT solver ( i.e. STP) but that requires infrastructure changes.
Diffstat (limited to 'test/Feature/MultiMkSym.c')
0 files changed, 0 insertions, 0 deletions