[fix, bitwuzla] Implemented sign extension for widths greater then 64.

S1eGa · Nov 20, 2023 · a9ae83d · a9ae83d
1 parent 7b524ea
commit a9ae83d
Showing 1 changed file with 12 additions and 3 deletions.
diff --git a/lib/Solver/BitwuzlaBuilder.cpp b/lib/Solver/BitwuzlaBuilder.cpp
@@ -284,9 +284,18 @@ Term BitwuzlaBuilder::bvSignExtend(Term src, unsigned width) {
   Term srcAsBv = castToBitVector(src);
   unsigned src_width = srcAsBv.sort().bv_size();
   assert(src_width <= width && "attempted to extend longer data");
-  assert(width < CHAR_BIT * sizeof(uint64_t) &&
-         "bitwuzla does not support sext for width more than 64 bit");
-  return mk_term(Kind::BV_SIGN_EXTEND, {srcAsBv}, {width - src_width});
+
+  if (width <= 64) {
+    return mk_term(Kind::BV_SIGN_EXTEND, {srcAsBv}, {width - src_width});
+  }
+
+  Term signBit = bvBoolExtract(srcAsBv, src_width - 1);
+  Term zeroExtended =
+      mk_term(Kind::BV_CONCAT, {bvZero(width - src_width), src});
+  Term oneExtended =
+      mk_term(Kind::BV_CONCAT, {bvMinusOne(width - src_width), src});
+
+  return mk_term(Kind::ITE, {signBit, oneExtended, zeroExtended});
 }
 
 Term BitwuzlaBuilder::writeExpr(Term array, Term index, Term value) {