Skip to content

Commit

Permalink
Fix #25 reported by @liammachado .
Browse files Browse the repository at this point in the history
In `SimpleExprBuilder.ConstantBV()` the check of the absolute value
was off by one.
  • Loading branch information
Dan Liew committed Apr 6, 2017
1 parent 83b5276 commit bee2776
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
4 changes: 2 additions & 2 deletions src/Symbooglix/Expr/SimpleExprBuilder.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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 );
Expand Down

0 comments on commit bee2776

Please sign in to comment.