[SMTChecker] Reset checked/unchecked flag to the default value when inlining function in BMC

libsolidity/formal/BMC.cpp

@@ -528,7 +528,9 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 		// is that there we don't have `_funCall`.
 		pushCallStack({funDef, &_funCall});
 		pushPathCondition(currentPathConditions());
+		auto oldChecked = std::exchange(m_checked, true);
 		funDef->accept(*this);
+		m_checked = oldChecked;
 		popPathCondition();
 	}
 

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