diff --git a/src/ExprBuilderTests/SimpleExprBuilderTests/ConstantsSimpleBuilder.cs b/src/ExprBuilderTests/SimpleExprBuilderTests/ConstantsSimpleBuilder.cs index 5854282..2971bda 100644 --- a/src/ExprBuilderTests/SimpleExprBuilderTests/ConstantsSimpleBuilder.cs +++ b/src/ExprBuilderTests/SimpleExprBuilderTests/ConstantsSimpleBuilder.cs @@ -161,6 +161,7 @@ private void _PositiveBV(int decimalValue, int width, string expectedString) [TestCase(-5, 4, "11bv4")] [TestCase(-11, 32, "4294967285bv32")] [TestCase(0, 4, "0bv4")] + [TestCase(-8, 4, "8bv4")] public void NegativeBV(int decimalValue, int width, string expectedString) { _NegativeBV(decimalValue, width, expectedString); diff --git a/src/Symbooglix/Expr/SimpleExprBuilder.cs b/src/Symbooglix/Expr/SimpleExprBuilder.cs index 53eab97..1cfaa2a 100644 --- a/src/Symbooglix/Expr/SimpleExprBuilder.cs +++ b/src/Symbooglix/Expr/SimpleExprBuilder.cs @@ -113,14 +113,14 @@ public LiteralExpr ConstantBV(BigInteger decimalValue, int bitWidth) // // The rule is basically this: // - // decimal_rep_for_bits = (2^m - x) mod (2^m) + // decimal_rep_for_bits = (2^m - |x|) mod (2^m) if (bitWidth <=1) throw new ArgumentException("Decimal value cannot be represented in the requested number of bits"); var abs = BigInteger.Abs(decimalValue); - if (abs >= BigInteger.Pow(2, bitWidth -1)) + if (abs > BigInteger.Pow(2, bitWidth -1)) throw new ArgumentException("Decimal value cannot be represented in the requested number of bits"); var result = ( twoToPowerOfBits - abs );