BitvectorFormulaManager: fix ROL/ROR for cases, where rotation is done by bitsize^2-1.

The bug should when using small bitsize (=2) and rotate by 1.

Author: kfriedberger

src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java

@@ -340,7 +340,7 @@ public BitvectorFormula rotateLeft(BitvectorFormula pNumber, BitvectorFormula pT
   protected TFormulaInfo rotateLeft(TFormulaInfo pNumber, TFormulaInfo pToRotate) {
     int length = getLength(wrap(pNumber));
     final TFormulaInfo lengthAsBv = makeBitvectorImpl(length, length);
-    final TFormulaInfo toRotateInRange = smodulo(pToRotate, lengthAsBv);
+    final TFormulaInfo toRotateInRange = remainder(pToRotate, lengthAsBv, false);
     return or(
         shiftLeft(pNumber, toRotateInRange),
         shiftRight(pNumber, subtract(lengthAsBv, toRotateInRange), false));
@@ -373,7 +373,7 @@ public BitvectorFormula rotateRight(BitvectorFormula pNumber, BitvectorFormula p
   protected TFormulaInfo rotateRight(TFormulaInfo pNumber, TFormulaInfo pToRotate) {
     int length = getLength(wrap(pNumber));
     final TFormulaInfo lengthAsBv = makeBitvectorImpl(length, length);
-    final TFormulaInfo toRotateInRange = smodulo(pToRotate, lengthAsBv);
+    final TFormulaInfo toRotateInRange = remainder(pToRotate, lengthAsBv, false);
     return or(
         shiftRight(pNumber, toRotateInRange, false),
         shiftLeft(pNumber, subtract(lengthAsBv, toRotateInRange)));