Fix internal error when deleting struct member of function type

test/libsolidity/smtCheckerTests/abi/abi_encode_function.sol

@@ -6,4 +6,3 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6031: (54-60): Internal error: Expression undefined for SMT solver.

test/libsolidity/smtCheckerTests/functions/getters/function.sol

@@ -15,5 +15,6 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (152-170): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f()\n    e() -- untrusted external call\n    g() -- untrusted external call
-// Warning 6328: (262-278): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f()\n    e() -- untrusted external call\n    g() -- untrusted external call\n    e() -- untrusted external call
+// Warning 8364: (140-146): Assertion checker does not yet implement type function () view external returns (function () external returns (uint256))
+// Warning 6328: (152-170): CHC: Assertion violation happens here.
+// Warning 6328: (262-278): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol

@@ -19,4 +19,5 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 2072: (146-183): Unused local variable.
-// Warning 6328: (234-269): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 0, f: 0}\nd = 0\nf = 0\n\nTransaction trace:\nC.constructor()\nState: s = {d: 0, f: 0}\nC.test()
+// Warning 8364: (187-193): Assertion checker does not yet implement type function () view external returns (contract D,function () external returns (uint256))
+// Warning 6328: (234-269): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/imports/import_library_2.sol

@@ -25,4 +25,4 @@ contract ERC20 {
 // ====
 // SMTEngine: all
 // ----
-// Warning 3944: (ERC20.sol:157-162): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\namount = 1\n\nTransaction trace:\nERC20.constructor()\nERC20.transferFrom(1){ msg.sender: 0x52f6 }\n    SafeMath.sub(0, 1) -- internal call
+// Warning 3944: (ERC20.sol:157-162): CHC: Underflow (resulting value less than 0) happens here.

test/libsolidity/smtCheckerTests/operators/delete_function_type_1.sol

@@ -0,0 +1,16 @@
+struct S {
+    function() e;
+}
+
+contract C {
+    S s;
+    function() f;
+
+    constructor() {
+        delete s.e;
+        assert(s.e == f); // should fail for now because function pointer comparisons are not supported
+    }
+}
+// ----
+// Warning 7229: (128-136): Assertion checker does not yet implement the type function () for comparisons
+// Warning 6328: (121-137): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/delete_function_type_2.sol

@@ -0,0 +1,13 @@
+contract C {
+    mapping (uint => function()) m;
+    function() f;
+
+    constructor() {
+        m[2] = f;
+        delete m[2];
+        assert(m[2] == f); // should fail for now because function pointer comparisons are not supported
+    }
+}
+// ----
+// Warning 7229: (142-151): Assertion checker does not yet implement the type function () for comparisons
+// Warning 6328: (135-152): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/operators/delete_function_type_3.sol

@@ -0,0 +1,19 @@
+contract C {
+    function()[] arr;
+    function() f;
+
+    constructor() {
+        arr.push();
+        arr.push();
+        arr[1] = f;
+        delete arr[1];
+        assert(arr[1] == f); // should fail for now because function pointer comparisons are not supported
+    }
+}
+// ----
+// Warning 8364: (82-90): Assertion checker does not yet implement type function (function ()[] storage pointer) returns (function ())
+// Warning 8364: (102-110): Assertion checker does not yet implement type function (function ()[] storage pointer) returns (function ())
+// Warning 7229: (172-183): Assertion checker does not yet implement the type function () for comparisons
+// Warning 6368: (149-155): CHC: Out of bounds access happens here.
+// Warning 6368: (172-178): CHC: Out of bounds access happens here.
+// Warning 6328: (165-184): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/address_transfer.sol

@@ -11,5 +11,5 @@ contract C
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (162-186): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0x0\nx = 100\n\nTransaction trace:\nC.constructor()\nC.f(0x0)
+// Warning 6328: (162-186): CHC: Assertion violation happens here.
 // Warning 1236: (98-113): BMC: Insufficient funds happens here.

test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol

@@ -15,4 +15,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (245-270): CHC: Assertion violation happens here.\nCounterexample:\narray = [[200]]\nx = 0\ny = 0\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: array = []\nC.a()\nState: array = [[0]]\nC.f(0, 0, 0, 0)
+// Warning 6328: (245-270): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol

@@ -16,4 +16,4 @@ contract C
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (318-346): CHC: Assertion violation happens here.\nCounterexample:\narray = [[[200]]]\nx = 0\ny = 0\nz = 0\nt = 0\nw = 0\nv = 0\n\nTransaction trace:\nC.constructor()\nState: array = []\nC.p()\nState: array = [[[0]]]\nC.f(0, 0, 0, 0, 0, 0)
+// Warning 6328: (318-346): CHC: Assertion violation happens here.