Don't erase things for BMC if function call is staticcall

libsolidity/formal/BMC.cpp

@@ -587,6 +587,11 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 			_funCall.location(),
 			"BMC does not yet implement this type of function call."
 		);
+	else if (funType.kind() == FunctionType::Kind::BareStaticCall)
+	{
+		// Do nothing here.
+		// Neither storage nor balances should be modified.
+	}
 	else
 	{
 		m_externalFunctionCallHappened = true;

test/libsolidity/smtCheckerTests/bmc_coverage/call_balance.sol

@@ -0,0 +1,13 @@
+contract C {
+	function f(address _a) public {
+		uint b1 = address(this).balance;
+		_a.call("");
+		uint b2 = address(this).balance;
+		assert(b1 == b2); // should fail
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 9302: (83-94): Return value of low-level calls not used.
+// Warning 4661: (133-149): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/bmc_coverage/call_state_var.sol

@@ -0,0 +1,13 @@
+contract C {
+	uint x;
+	function f(address _a) public {
+		x = 2;
+		_a.call("");
+		assert(x == 2); // should fail
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 9302: (66-77): Return value of low-level calls not used.
+// Warning 4661: (81-95): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/bmc_coverage/staticcall_balance.sol

@@ -0,0 +1,12 @@
+contract C {
+	function f(address _a) public view {
+		uint b1 = address(this).balance;
+		_a.staticcall("");
+		uint b2 = address(this).balance;
+		assert(b1 == b2); // should hold
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 9302: (88-105): Return value of low-level calls not used.

test/libsolidity/smtCheckerTests/bmc_coverage/staticcall_state_var.sol

@@ -0,0 +1,12 @@
+contract C {
+	uint x;
+	function f(address _a) public {
+		x = 2;
+		_a.staticcall("");
+		assert(x == 2); // should hold
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 9302: (66-83): Return value of low-level calls not used.