[fix, bitwuzla, tmp] Removed optimization on Bitwuzla's AShr operation.

S1eGa · Nov 20, 2023 · eef8d8c · eef8d8c
1 parent a7314d5
commit eef8d8c
Showing 1 changed file with 13 additions and 9 deletions.
diff --git a/lib/Solver/BitwuzlaBuilder.cpp b/lib/Solver/BitwuzlaBuilder.cpp
@@ -804,15 +804,19 @@ Term BitwuzlaBuilder::constructActual(ref<Expr> e, int *width_out) {
     Term left = castToBitVector(construct(ase->left, width_out));
     assert(*width_out != 1 && "uncanonicalized ashr");
 
-    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
-      unsigned shift = (unsigned)CE->getLimitedValue();
-      Term signedBool = bvBoolExtract(left, *width_out - 1);
-      return constructAShrByConstant(left, shift, signedBool);
-    } else {
-      int shiftWidth;
-      Term amount = construct(ase->right, &shiftWidth);
-      return bvVarArithRightShift(left, amount);
-    }
+    int shiftWidth;
+    Term amount = construct(ase->right, &shiftWidth);
+    return bvVarArithRightShift(left, amount);
+
+    // if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
+    //   unsigned shift = (unsigned)CE->getLimitedValue();
+    //   Term signedBool = bvBoolExtract(left, *width_out - 1);
+    //   return constructAShrByConstant(left, shift, signedBool);
+    // } else {
+    //   int shiftWidth;
+    //   Term amount = construct(ase->right, &shiftWidth);
+    //   return bvVarArithRightShift(left, amount);
+    // }
   }
 
     // Comparison