From b058af7f05be473e31a82fa1cdacf675eea784da Mon Sep 17 00:00:00 2001
From: Hristina Palikareva <h.palikareva@imperial.ac.uk>
Date: Thu, 24 Apr 2014 15:32:34 +0100
Subject: Fixed creation of arrays with variable domains and ranges in
 STPBuilder and MetaSMTBuilder.

---
 lib/Solver/STPBuilder.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'lib/Solver/STPBuilder.cpp')

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));
-- 
cgit 1.4.1