fix bitvec err for sse

SVF-tools · Jul 25, 2023 · 3aec7a3 · 3aec7a3
1 parent 753e7cc
commit 3aec7a3
Showing 1 changed file with 7 additions and 12 deletions.
diff --git a/svf/include/AbstractExecution/BoundedZ3Expr.h b/svf/include/AbstractExecution/BoundedZ3Expr.h
@@ -29,6 +29,7 @@
 
 #ifndef SVF_BOUNDEDZ3EXPR_H
 #define SVF_BOUNDEDZ3EXPR_H
+#define MaxBvLen 64
 
 #include "Util/Z3Expr.h"
 
@@ -248,20 +249,17 @@ class BoundedZ3Expr : public Z3Expr
 
     friend BoundedZ3Expr operator^(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs)
     {
-        s64_t maxBvLen  = 64;
-        return bv2int(int2bv(maxBvLen, lhs.getExpr()) ^ int2bv(maxBvLen, rhs.getExpr()), true);
+        return bv2int(int2bv(MaxBvLen, lhs.getExpr()) ^ int2bv(MaxBvLen, rhs.getExpr()), true);
     }
 
     friend BoundedZ3Expr operator&(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs)
     {
-        s64_t maxBvLen  = 64;
-        return bv2int(int2bv(maxBvLen, lhs.getExpr()) & int2bv(maxBvLen, rhs.getExpr()), true);
+        return bv2int(int2bv(MaxBvLen, lhs.getExpr()) & int2bv(MaxBvLen, rhs.getExpr()), true);
     }
 
     friend BoundedZ3Expr operator|(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs)
     {
-        s64_t maxBvLen  = 64;
-        return bv2int(int2bv(maxBvLen, lhs.getExpr()) | int2bv(maxBvLen, rhs.getExpr()), true);
+        return bv2int(int2bv(MaxBvLen, lhs.getExpr()) | int2bv(MaxBvLen, rhs.getExpr()), true);
     }
 
     friend BoundedZ3Expr ashr(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs)
@@ -274,8 +272,7 @@ class BoundedZ3Expr : public Z3Expr
             return ite(lhs.getExpr() >= 0, BoundedZ3Expr(0), BoundedZ3Expr(-1));
         else
         {
-            s64_t maxBvLen  = 64;
-            return bv2int(ashr(int2bv(maxBvLen, lhs.getExpr()), int2bv(maxBvLen, rhs.getExpr())), true);
+            return bv2int(ashr(int2bv(MaxBvLen, lhs.getExpr()), int2bv(MaxBvLen, rhs.getExpr())), true);
         }
     }
 
@@ -289,15 +286,13 @@ class BoundedZ3Expr : public Z3Expr
             return ite(lhs.getExpr() >= 0, plus_infinity(), minus_infinity());
         else
         {
-            s64_t maxBvLen  = 64;
-            return bv2int(shl(int2bv(maxBvLen, lhs.getExpr()), int2bv(maxBvLen, rhs.getExpr())), true);
+            return bv2int(shl(int2bv(MaxBvLen, lhs.getExpr()), int2bv(MaxBvLen, rhs.getExpr())), true);
         }
     }
 
     friend BoundedZ3Expr lshr(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs)
     {
-        s64_t maxBvLen  = 64;
-        return bv2int(lshr(int2bv(maxBvLen, lhs.getExpr()), int2bv(maxBvLen, rhs.getExpr())), true);
+        return bv2int(lshr(int2bv(MaxBvLen, lhs.getExpr()), int2bv(MaxBvLen, rhs.getExpr())), true);
     }
 
     friend BoundedZ3Expr int2bv(u32_t n, const BoundedZ3Expr &e)