diff options
| author | Dan Liew <delcypher@gmail.com> | 2014-04-24 17:26:51 +0100 |
|---|---|---|
| committer | Dan Liew <delcypher@gmail.com> | 2014-04-24 17:26:51 +0100 |
| commit | 7ce1eed6334be42dae30435acfae4f98f6ac3950 (patch) | |
| tree | deac2388bba38541741efc6ef171418286442061 /lib/Solver/STPBuilder.cpp | |
| parent | 9dd4766a3f58070501ed6498e6aa42c14776cc0f (diff) | |
| parent | b058af7f05be473e31a82fa1cdacf675eea784da (diff) | |
| download | klee-7ce1eed6334be42dae30435acfae4f98f6ac3950.tar.gz | |
Merge pull request #121 from hpalikareva/domain-range-metasmt
Fixed creation of arrays with variable domains and ranges in STPBuilder ...
Diffstat (limited to 'lib/Solver/STPBuilder.cpp')
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index ebc096df..e4a21f74 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -553,7 +553,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { case Expr::Read: { ReadExpr *re = cast<ReadExpr>(e); - *width_out = 8; + assert(re && re->updates.root); + *width_out = re->updates.root->getRange(); return vc_readExpr(vc, getArrayForUpdate(re->updates.root, re->updates.head), construct(re->index, 0)); |