Gidon's genius idea to largely reduce the time consumption

Author: DonggeLiu

claripy/backends/backend_z3_quick_sampler.py

@@ -82,7 +82,7 @@ def bv_sampler(self, solver, exprs):
 
         # solver = self.solver()
         solver.add(result == target)
-        solver.minimize(self._bv_count(delta))
+        solver.minimize(z3.BV2Int(delta))
         results = set()
 
         while True: