Fix variable shifting behavior with different sizes

Generated STP equality expressions have to be the same type.
If a shift with different types as operands was used,
therefore equality expressions of different width were generated.

Beside avoiding the different sizes, this patch restores the
original behavior to extract just the part involved in shifting
and therefore should generate smaller expressions.

Enable sdiv test case

1 files changed, 2 insertions, 0 deletions

diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h
index 3b17ccf1..5be34029 100644
--- a/lib/Solver/STPBuilder.h
+++ b/lib/Solver/STPBuilder.h
@@ -93,6 +93,8 @@ private:
   ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift);
   ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift);
   ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift);
+  ExprHandle extractPartialShiftValue(ExprHandle shift, unsigned width,
+                                      unsigned &shiftBits);
 
   ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, 
                                      ExprHandle isSigned);