diff options
| author | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2014-04-24 15:32:34 +0100 |
|---|---|---|
| committer | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2014-04-24 15:32:34 +0100 |
| commit | b058af7f05be473e31a82fa1cdacf675eea784da (patch) | |
| tree | deac2388bba38541741efc6ef171418286442061 /lib/Solver/STPBuilder.cpp | |
| parent | 9dd4766a3f58070501ed6498e6aa42c14776cc0f (diff) | |
| download | klee-b058af7f05be473e31a82fa1cdacf675eea784da.tar.gz | |
Fixed creation of arrays with variable domains and ranges in STPBuilder and MetaSMTBuilder.
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)); |