STPBuilder: fix ConstantExpr builder for the case where width>64 but

is not a multiple of 64.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@153473 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 5 insertions, 5 deletions

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index f150d2a5..28b5c1a5 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -478,13 +478,13 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     if (*width_out <= 64)
       return bvConst64(*width_out, CE->getZExtValue());
 
-    // FIXME: Optimize?
     ref<ConstantExpr> Tmp = CE;
     ExprHandle Res = bvConst64(64, Tmp->Extract(0, 64)->getZExtValue());
-    for (unsigned i = (*width_out / 64) - 1; i; --i) {
-      Tmp = Tmp->LShr(ConstantExpr::alloc(64, Tmp->getWidth()));
-      Res = vc_bvConcatExpr(vc, bvConst64(std::min(64U, Tmp->getWidth()),
-                                          Tmp->Extract(0, 64)->getZExtValue()),
+    while (Tmp->getWidth() > 64) {
+      Tmp = Tmp->Extract(64, Tmp->getWidth()-64);
+      unsigned Width = std::min(64U, Tmp->getWidth());
+      Res = vc_bvConcatExpr(vc, bvConst64(Width,
+                                        Tmp->Extract(0, Width)->getZExtValue()),
                             Res);
     }
     return Res;