Merge pull request #10777 from blishko/smt-fix-checked

[SMTChecker] Fix BMC crash related to `unchecked` blocks

test/libsolidity/smtCheckerTests/bmc_coverage/unchecked_function_call_with_unchecked_block.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x) internal pure {
+		unchecked {
+			uint y = x - 1;
+			assert(y < x); // should fail, underflow can happen, we are inside unchecked block
+		}
+	}
+	function g(uint x) public pure {
+		unchecked { f(x); }
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (117-130): BMC: Assertion violation happens here.
+// Warning 4661: (117-130): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/unchecked/unchecked_double_with_modifier.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	modifier m() {
+		unchecked{}
+		_;
+	}
+
+	function t() m internal pure {}
+
+	function f() public pure {
+		unchecked { t(); }
+	}
+}
+
+
+// ----

test/libsolidity/smtCheckerTests/unchecked/unchecked_function_call_with_unchecked_block.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x) internal pure {
+		unchecked {
+			uint y = x - 1;
+			assert(y < x); // should fail, underflow can happen, we are inside unchecked block
+		}
+	}
+	function g(uint x) public pure {
+		unchecked { f(x); }
+	}
+}
+// ----
+// Warning 6328: (117-130): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    C.f(0) -- internal call