Skip to content

Commit

Permalink
split out passing and failing mul tests
Browse files Browse the repository at this point in the history
  • Loading branch information
mshrieve committed Oct 22, 2020
1 parent 0f9d83b commit 8ee8e07
Showing 1 changed file with 9 additions and 1 deletion.
10 changes: 9 additions & 1 deletion specs/fixedPoint.spec
Original file line number Diff line number Diff line change
Expand Up @@ -29,11 +29,19 @@ description "test subtraction"
assert (a >= b && a - b == c) || (b - a == c), "failed subtraction test";
}

rule testMultiplication(uint256 a, uint256 b)
rule testMultiplicationWithRequire(uint256 a, uint256 b)
description "test multiplication"
{
uint256 c = sinvoke testMul(a, b, 18);
mathint expected = (a * b) / 1000000000000000000;
require(a*b*2000000000000000000 < MAXINT());
assert c == expected, "failed multiplication test";
}

rule testMultiplicationWithoutRequire(uint256 a, uint256 b)
description "test multiplication"
{
uint256 c = sinvoke testMul(a, b, 18);
mathint expected = (a * b) / 1000000000000000000;
assert c == expected, "failed multiplication test";
}

0 comments on commit 8ee8e07

Please sign in to comment.