From cf8e311e1255b2515c50ab5043551498703acce3 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Wed, 30 Mar 2011 11:08:09 +0000
Subject: Bug fix in STPBuilder. Patch submitted by David Ramos, thanks!
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@128532 91177308-0d34-0410-b5e6-96231b3b80d8
---
lib/Solver/STPBuilder.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
(limited to 'lib/Solver/STPBuilder.cpp')
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index de53816c..f150d2a5 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -528,7 +528,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
ExprHandle src = construct(ee->expr, width_out);
*width_out = ee->getWidth();
if (*width_out==1) {
- return bvBoolExtract(src, 0);
+ return bvBoolExtract(src, ee->offset);
} else {
return vc_bvExtract(vc, src, ee->offset + *width_out - 1, ee->offset);
}
--
cgit 1.4.1