diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index ddf1152a3..d7742084a 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/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;
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/call_balance.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/call_balance.sol
new file mode 100644
index 000000000..b0f383a14
--- /dev/null
+++ b/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.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/call_state_var.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/call_state_var.sol
new file mode 100644
index 000000000..3e58eea11
--- /dev/null
+++ b/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.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/staticcall_balance.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/staticcall_balance.sol
new file mode 100644
index 000000000..167cea38c
--- /dev/null
+++ b/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.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/staticcall_state_var.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/staticcall_state_var.sol
new file mode 100644
index 000000000..50f959997
--- /dev/null
+++ b/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.