Skip to content

Commit 1655626

Browse files
committed
Remove counterexample from test.
1 parent b49f486 commit 1655626

File tree

1 file changed

+5
-4
lines changed

1 file changed

+5
-4
lines changed

test/libsolidity/smtCheckerTests/userTypes/fixedpoint.sol

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -67,8 +67,9 @@ contract TestFixedMath {
6767
}
6868
// ====
6969
// SMTEngine: all
70+
// SMTIgnoreCex: yes
7071
// ----
71-
// Warning 6328: (1886-1970): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTestFixedMath.constructor()\nTestFixedMath.f()\n TestFixedMath.add(0, 0) -- internal call\n FixedMath.add(0, 0) -- internal call\n TestFixedMath.add(25, 45) -- internal call\n FixedMath.add(25, 45) -- internal call\n TestFixedMath.add(25, 45) -- internal call\n FixedMath.add(25, 45) -- internal call
72-
// Warning 6328: (2165-2266): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTestFixedMath.constructor()\nTestFixedMath.g()\n TestFixedMath.mul(340282366920938463463374607431768211456, 20) -- internal call\n FixedMath.mul(340282366920938463463374607431768211456, 20) -- internal call\n TestFixedMath.mul(340282366920938463463374607431768211456, 20) -- internal call\n FixedMath.mul(340282366920938463463374607431768211456, 20) -- internal call
73-
// Warning 6328: (2675-2791): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTestFixedMath.constructor()\nTestFixedMath.h()\n TestFixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call\n FixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call\n TestFixedMath.floor(115792089237316195423570985008687907853269984665640564039457584007913129639935) -- internal call\n FixedMath.floor(115792089237316195423570985008687907853269984665640564039457584007913129639935) -- internal call\n TestFixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call\n FixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call
74-
// Warning 6328: (3161-3212): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTestFixedMath.constructor()\nTestFixedMath.i()\n TestFixedMath.toUFixed256x18(0) -- internal call\n FixedMath.toUFixed256x18(0) -- internal call\n TestFixedMath.toUFixed256x18(5) -- internal call\n FixedMath.toUFixed256x18(5) -- internal call\n TestFixedMath.toUFixed256x18(115792089237316195423570985008687907853269984665640564039457) -- internal call\n FixedMath.toUFixed256x18(115792089237316195423570985008687907853269984665640564039457) -- internal call\n TestFixedMath.toUFixed256x18(5) -- internal call\n FixedMath.toUFixed256x18(5) -- internal call
72+
// Warning 6328: (1886-1970): CHC: Assertion violation happens here.
73+
// Warning 6328: (2165-2266): CHC: Assertion violation happens here.
74+
// Warning 6328: (2675-2791): CHC: Assertion violation happens here.
75+
// Warning 6328: (3161-3212): CHC: Assertion violation happens here.

0 commit comments

Comments
 (0)