fix: crytic#13 add_test_range & sub_test_range false negatives

beber89 · Mar 15, 2023 · c02e20d · c02e20d
1 parent b167773
commit c02e20d
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol b/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol
@@ -302,7 +302,8 @@ contract CryticABDKMath64x64Properties {
         int128 result;
         try this.add(x, y) {
             result = this.add(x, y);
-            assert(result <= MAX_64x64 && result >= MIN_64x64);
+            assert(!(x >= 0 && y >= 0)  || (result >= x && result >= y));
+            assert(!(x < 0 && y < 0)  || (result < y && result < x));
         } catch {
             // If it reverts, just ignore
         }
@@ -431,7 +432,8 @@ contract CryticABDKMath64x64Properties {
         int128 result;
         try this.sub(x, y) {
             result = this.sub(x, y);
-            assert(result <= MAX_64x64 && result >= MIN_64x64);
+            assert(!(x >= 0 && y <= 0)  || (result >= x && result >= neg (y)));
+            assert(!(x < 0 && y >= 0)  || (result < neg(y) && result <= x));
         } catch {
             // If it reverts, just ignore
         }