User-defined operators: Tests

2023-10-03 13:03:40 +00:00 · 2023-02-22 00:40:03 +01:00
parent 5b5e853ea0
commit aba5ac5e2a
114 changed files with 3956 additions and 1 deletions
@@ -0,0 +1,16 @@
+type U is uint;
+using {div as /} for U global;
+
+function div(U x, U y) pure returns (U) {
+    return U.wrap(U.unwrap(x) / U.unwrap(y));
+}
+
+contract C {
+    function f(U x, U y) public pure returns (U) {
+        return x / y; // FIXME: should detect div by zero
+    }
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6756: (218-223): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
@@ -0,0 +1,19 @@
+type U is uint;
+using {div as /} for U global;
+
+function div(U x, U y) pure returns (U) {
+    if (U.unwrap(y) == 0)
+        return U.wrap(0);
+
+    return U.wrap(U.unwrap(x) / U.unwrap(y));
+}
+
+contract C {
+    function f(U x, U y) public pure returns (U) {
+        return x / y; // no div by zero possible here
+    }
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6756: (271-276): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
@@ -0,0 +1,104 @@
+type I16 is int16;
+using {
+    bitor as |, bitand as &, bitxor as ^, bitnot as ~,
+    add as +, sub as -, unsub as -, mul as *, div as /, mod as %,
+    eq as ==, noteq as !=, lt as <, gt as >, leq as <=, geq as >=
+} for I16 global;
+
+function bitor(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) | I16.unwrap(y)); }
+function bitand(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) & I16.unwrap(y)); }
+function bitxor(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) ^ I16.unwrap(y)); }
+function bitnot(I16 x) pure returns (I16) { return I16.wrap(~I16.unwrap(x)); }
+
+function add(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) + I16.unwrap(y)); }
+function sub(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) - I16.unwrap(y)); }
+function unsub(I16 x) pure returns (I16) { return I16.wrap(-I16.unwrap(x)); }
+function mul(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) * I16.unwrap(y)); }
+function div(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) / I16.unwrap(y)); }
+function mod(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) % I16.unwrap(y)); }
+
+function eq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) == I16.unwrap(y); }
+function noteq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) != I16.unwrap(y); }
+function lt(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) < I16.unwrap(y); }
+function gt(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) > I16.unwrap(y); }
+function leq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) <= I16.unwrap(y); }
+function geq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) >= I16.unwrap(y); }
+
+contract C {
+    I16 constant MINUS_TWO = I16.wrap(-2);
+    I16 constant ZERO = I16.wrap(0);
+    I16 constant ONE = I16.wrap(1);
+    I16 constant TWO = I16.wrap(2);
+    I16 constant THREE = I16.wrap(3);
+    I16 constant FOUR = I16.wrap(4);
+
+    function testBitwise() public pure {
+        assert(ONE | TWO == THREE); // FIXME: should hold
+        assert(ONE & THREE == ZERO); // FIXME: should hold
+        assert(TWO ^ TWO == ZERO); // FIXME: should hold
+        assert(~ONE == MINUS_TWO); // FIXME: should hold
+    }
+
+    function testArithmetic() public pure {
+        assert(TWO + TWO == FOUR); // FIXME: should hold
+        assert(TWO - TWO == ZERO); // FIXME: should hold
+        assert(-TWO == MINUS_TWO); // FIXME: should hold
+        assert(TWO * TWO == FOUR); // FIXME: should hold
+        assert(TWO / TWO == ONE); // FIXME: should hold
+        assert(TWO % TWO == ZERO); // FIXME: should hold
+    }
+
+    function testComparison() public pure {
+        assert(TWO == TWO); // FIXME: should hold
+        assert(!(TWO != TWO)); // FIXME: should hold
+        assert(!(TWO < TWO)); // FIXME: should hold
+        assert(!(TWO > TWO)); // FIXME: should hold
+        assert(TWO <= TWO); // FIXME: should hold
+        assert(TWO >= TWO); // FIXME: should hold
+    }
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6756: (2019-2028): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results.
+// Warning 6756: (2019-2037): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2077-2088): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results.
+// Warning 6756: (2077-2096): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2136-2145): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results.
+// Warning 6756: (2136-2153): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6156: (2193-2197): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results.
+// Warning 6756: (2193-2210): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2301-2310): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.
+// Warning 6756: (2301-2318): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2358-2367): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
+// Warning 6756: (2358-2375): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6156: (2415-2419): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
+// Warning 6756: (2415-2432): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2472-2481): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results.
+// Warning 6756: (2472-2489): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2529-2538): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
+// Warning 6756: (2529-2545): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2585-2594): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results.
+// Warning 6756: (2585-2602): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2693-2703): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2745-2755): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results.
+// Warning 6756: (2798-2807): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results.
+// Warning 6756: (2850-2859): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results.
+// Warning 6756: (2900-2910): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results.
+// Warning 6756: (2950-2960): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results.
+// Warning 6328: (2012-2038): CHC: Assertion violation happens here.
+// Warning 6328: (2070-2097): CHC: Assertion violation happens here.
+// Warning 6328: (2129-2154): CHC: Assertion violation happens here.
+// Warning 6328: (2186-2211): CHC: Assertion violation happens here.
+// Warning 6328: (2294-2319): CHC: Assertion violation happens here.
+// Warning 6328: (2351-2376): CHC: Assertion violation happens here.
+// Warning 6328: (2408-2433): CHC: Assertion violation happens here.
+// Warning 6328: (2465-2490): CHC: Assertion violation happens here.
+// Warning 6328: (2522-2546): CHC: Assertion violation happens here.
+// Warning 6328: (2578-2603): CHC: Assertion violation happens here.
+// Warning 6328: (2686-2704): CHC: Assertion violation happens here.
+// Warning 6328: (2736-2757): CHC: Assertion violation happens here.
+// Warning 6328: (2789-2809): CHC: Assertion violation happens here.
+// Warning 6328: (2841-2861): CHC: Assertion violation happens here.
+// Warning 6328: (2893-2911): CHC: Assertion violation happens here.
+// Warning 6328: (2943-2961): CHC: Assertion violation happens here.
@@ -0,0 +1,104 @@
+type I16 is int16;
+using {
+    bitor as |, bitand as &, bitxor as ^, bitnot as ~,
+    add as +, sub as -, unsub as -, mul as *, div as /, mod as %,
+    eq as ==, noteq as !=, lt as <, gt as >, leq as <=, geq as >=
+} for I16 global;
+
+function bitor(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) | I16.unwrap(y)); }
+function bitand(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) & I16.unwrap(y)); }
+function bitxor(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) ^ I16.unwrap(y)); }
+function bitnot(I16 x) pure returns (I16) { return I16.wrap(~I16.unwrap(x)); }
+
+function add(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) + I16.unwrap(y)); }
+function sub(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) - I16.unwrap(y)); }
+function unsub(I16 x) pure returns (I16) { return I16.wrap(-I16.unwrap(x)); }
+function mul(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) * I16.unwrap(y)); }
+function div(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) / I16.unwrap(y)); }
+function mod(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) % I16.unwrap(y)); }
+
+function eq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) == I16.unwrap(y); }
+function noteq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) != I16.unwrap(y); }
+function lt(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) < I16.unwrap(y); }
+function gt(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) > I16.unwrap(y); }
+function leq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) <= I16.unwrap(y); }
+function geq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) >= I16.unwrap(y); }
+
+contract C {
+    I16 constant MINUS_TWO = I16.wrap(-2);
+    I16 constant ZERO = I16.wrap(0);
+    I16 constant ONE = I16.wrap(1);
+    I16 constant TWO = I16.wrap(2);
+    I16 constant THREE = I16.wrap(3);
+    I16 constant FOUR = I16.wrap(4);
+
+    function testBitwise() public pure {
+        assert(ONE | TWO == FOUR); // should fail
+        assert(ONE & THREE == FOUR); // should fail
+        assert(TWO ^ TWO == FOUR); // should fail
+        assert(~ONE == FOUR); // should fail
+    }
+
+    function testArithmetic() public pure {
+        assert(TWO + THREE == FOUR); // should fail
+        assert(TWO - TWO == FOUR); // should fail
+        assert(-TWO == FOUR); // should fail
+        assert(TWO * THREE == FOUR); // should fail
+        assert(TWO / TWO == FOUR); // should fail
+        assert(TWO % TWO == FOUR); // should fail
+    }
+
+    function testComparison() public pure {
+        assert(!(TWO == TWO)); // should fail
+        assert(TWO != TWO); // should fail
+        assert(TWO < TWO); // should fail
+        assert(TWO > TWO); // should fail
+        assert(!(TWO <= TWO)); // should fail
+        assert(!(TWO >= TWO)); // should fail
+    }
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6756: (2019-2028): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results.
+// Warning 6756: (2019-2036): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2069-2080): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results.
+// Warning 6756: (2069-2088): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2121-2130): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results.
+// Warning 6756: (2121-2138): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6156: (2171-2175): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results.
+// Warning 6756: (2171-2183): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2267-2278): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.
+// Warning 6756: (2267-2286): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2319-2328): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
+// Warning 6756: (2319-2336): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6156: (2369-2373): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
+// Warning 6756: (2369-2381): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2414-2425): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results.
+// Warning 6756: (2414-2433): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2466-2475): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
+// Warning 6756: (2466-2483): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2516-2525): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results.
+// Warning 6756: (2516-2533): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2619-2629): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2663-2673): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results.
+// Warning 6756: (2706-2715): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results.
+// Warning 6756: (2748-2757): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results.
+// Warning 6756: (2792-2802): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results.
+// Warning 6756: (2838-2848): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results.
+// Warning 6328: (2012-2037): CHC: Assertion violation happens here.
+// Warning 6328: (2062-2089): CHC: Assertion violation happens here.
+// Warning 6328: (2114-2139): CHC: Assertion violation happens here.
+// Warning 6328: (2164-2184): CHC: Assertion violation happens here.
+// Warning 6328: (2260-2287): CHC: Assertion violation happens here.
+// Warning 6328: (2312-2337): CHC: Assertion violation happens here.
+// Warning 6328: (2362-2382): CHC: Assertion violation happens here.
+// Warning 6328: (2407-2434): CHC: Assertion violation happens here.
+// Warning 6328: (2459-2484): CHC: Assertion violation happens here.
+// Warning 6328: (2509-2534): CHC: Assertion violation happens here.
+// Warning 6328: (2610-2631): CHC: Assertion violation happens here.
+// Warning 6328: (2656-2674): CHC: Assertion violation happens here.
+// Warning 6328: (2699-2716): CHC: Assertion violation happens here.
+// Warning 6328: (2741-2758): CHC: Assertion violation happens here.
+// Warning 6328: (2783-2804): CHC: Assertion violation happens here.
+// Warning 6328: (2829-2850): CHC: Assertion violation happens here.
@@ -0,0 +1,105 @@
+type I16 is int16;
+using {
+    bitor as |, bitand as &, bitxor as ^, bitnot as ~,
+    add as +, sub as -, unsub as -, mul as *, div as /, mod as %,
+    eq as ==, noteq as !=, lt as <, gt as >, leq as <=, geq as >=
+} for I16 global;
+
+function bitor(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) | I16.unwrap(y)); }
+function bitand(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) & I16.unwrap(y)); }
+function bitxor(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) ^ I16.unwrap(y)); }
+function bitnot(I16 x) pure returns (I16) { return I16.wrap(~I16.unwrap(x)); }
+
+function add(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) + I16.unwrap(y)); }
+function sub(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) - I16.unwrap(y)); }
+function unsub(I16 x) pure returns (I16) { return I16.wrap(-I16.unwrap(x)); }
+function mul(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) * I16.unwrap(y)); }
+function div(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) / I16.unwrap(y)); }
+function mod(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) % I16.unwrap(y)); }
+
+function eq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) == I16.unwrap(y); }
+function noteq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) != I16.unwrap(y); }
+function lt(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) < I16.unwrap(y); }
+function gt(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) > I16.unwrap(y); }
+function leq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) <= I16.unwrap(y); }
+function geq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) >= I16.unwrap(y); }
+
+contract C {
+    function testBitwise(I16 x, I16 y) public pure {
+        assert(x | y == bitor(x, y)); // FIXME: should hold
+        assert(x & y == bitand(x, y)); // FIXME: should hold
+        assert(x ^ y == bitxor(x, y)); // FIXME: should hold
+        assert(~x == bitnot(x)); // FIXME: should hold
+    }
+
+    function testArithmetic(I16 x, I16 y) public pure {
+        assert(x + y == add(x, y)); // FIXME: should hold
+        assert(x - y == sub(x, y)); // FIXME: should hold
+        assert(-x == unsub(x)); // FIXME: should hold
+        assert(x * y == mul(x, y)); // FIXME: should hold
+        assert(x / y == div(x, y)); // FIXME: should hold
+        assert(x % y == mod(x, y)); // FIXME: should hold
+    }
+
+    function testComparison(I16 x, I16 y) public pure {
+        assert((x == y) == eq(x, y)); // FIXME: should hold
+        assert((x != y) == noteq(x, y)); // FIXME: should hold
+        assert((x < y) == lt(x, y)); // FIXME: should hold
+        assert((x > y) == gt(x, y)); // FIXME: should hold
+        assert((x <= y) == leq(x, y)); // FIXME: should hold
+        assert((x >= y) == geq(x, y)); // FIXME: should hold
+    }
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6756: (1803-1808): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results.
+// Warning 6756: (1803-1823): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (1863-1868): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results.
+// Warning 6756: (1863-1884): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (1924-1929): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results.
+// Warning 6756: (1924-1945): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6156: (1985-1987): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results.
+// Warning 6756: (1985-2000): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2103-2108): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.
+// Warning 6756: (2103-2121): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2161-2166): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
+// Warning 6756: (2161-2179): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6156: (2219-2221): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
+// Warning 6756: (2219-2233): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2273-2278): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results.
+// Warning 6756: (2273-2291): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2331-2336): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
+// Warning 6756: (2331-2349): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2389-2394): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results.
+// Warning 6756: (2389-2407): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2511-2517): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
+// Warning 6756: (2571-2577): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results.
+// Warning 6756: (2634-2639): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results.
+// Warning 6756: (2693-2698): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results.
+// Warning 6756: (2752-2758): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results.
+// Warning 6756: (2813-2819): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results.
+// Warning 3944: (679-708): CHC: Underflow (resulting value less than -32768) happens here.
+// Warning 4984: (679-708): CHC: Overflow (resulting value larger than 32767) happens here.
+// Warning 3944: (777-806): CHC: Underflow (resulting value less than -32768) happens here.
+// Warning 4984: (777-806): CHC: Overflow (resulting value larger than 32767) happens here.
+// Warning 3944: (953-982): CHC: Underflow (resulting value less than -32768) happens here.
+// Warning 4984: (953-982): CHC: Overflow (resulting value larger than 32767) happens here.
+// Warning 4281: (1051-1080): CHC: Division by zero happens here.
+// Warning 4281: (1149-1178): CHC: Division by zero happens here.
+// Warning 6328: (1796-1824): CHC: Assertion violation happens here.
+// Warning 6328: (1856-1885): CHC: Assertion violation happens here.
+// Warning 6328: (1917-1946): CHC: Assertion violation happens here.
+// Warning 6328: (1978-2001): CHC: Assertion violation happens here.
+// Warning 6328: (2096-2122): CHC: Assertion violation happens here.
+// Warning 6328: (2154-2180): CHC: Assertion violation happens here.
+// Warning 6328: (2212-2234): CHC: Assertion violation happens here.
+// Warning 6328: (2266-2292): CHC: Assertion violation happens here.
+// Warning 6328: (2324-2350): CHC: Assertion violation happens here.
+// Warning 6328: (2382-2408): CHC: Assertion violation happens here.
+// Warning 6328: (2503-2531): CHC: Assertion violation happens here.
+// Warning 6328: (2563-2594): CHC: Assertion violation happens here.
+// Warning 6328: (2626-2653): CHC: Assertion violation happens here.
+// Warning 6328: (2685-2712): CHC: Assertion violation happens here.
+// Warning 6328: (2744-2773): CHC: Assertion violation happens here.
+// Warning 6328: (2805-2834): CHC: Assertion violation happens here.
@@ -0,0 +1,23 @@
+type U8 is uint8;
+using {add as +} for U8 global;
+
+function add(U8 x, U8 y) pure returns (U8) {
+    return U8.wrap(U8.unwrap(x) + U8.unwrap(y)); // FIXME: should detect possible overflow here
+}
+
+contract C {
+    U8 x = U8.wrap(254);
+
+    function inc() public {
+        x = x + U8.wrap(1); // FIXME: should detect possible overflow here
+    }
+
+    function check() view public {
+        U8 y = x;
+        assert(U8.unwrap(y) < 256);
+    }
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6756: (274-288): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.