diff options
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 10 |
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; |