diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index a25a5d373..bc53c7126 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -2960,9 +2960,6 @@ vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _f
 
 void SMTEncoder::collectFreeFunctions(set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
 {
-	if (!m_freeFunctions.empty())
-		return;
-
 	for (auto source: _sources)
 		for (auto node: source->nodes())
 			if (auto function = dynamic_cast<FunctionDefinition const*>(node.get()))
diff --git a/test/libsolidity/smtCheckerTests/imports/import_free_functions.sol b/test/libsolidity/smtCheckerTests/imports/import_free_functions.sol
new file mode 100644
index 000000000..4eec2c76a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/imports/import_free_functions.sol
@@ -0,0 +1,23 @@
+==== Source: Address.sol ====
+pragma solidity ^0.8.0;
+function s() pure {}
+==== Source: ERC20.sol ====
+pragma solidity ^0.8.0;
+
+import "./Address.sol";
+
+function sub(uint256 a, uint256 b) pure returns (uint256) {
+    return a - b;
+}
+
+contract ERC20 {
+    mapping (address => uint256) private _balances;
+
+    function transferFrom(uint256 amount) public view {
+        sub(_balances[msg.sender], amount);
+    }
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 3944: (ERC20.sol:121-126): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\namount = 1\n\nTransaction trace:\nERC20.constructor()\nERC20.transferFrom(1)\n    ERC20.sol:sub(0, 1) -- internal call
diff --git a/test/libsolidity/smtCheckerTests/imports/import_library_2.sol b/test/libsolidity/smtCheckerTests/imports/import_library_2.sol
new file mode 100644
index 000000000..d5c42dad6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/imports/import_library_2.sol
@@ -0,0 +1,28 @@
+==== Source: Address.sol ====
+pragma solidity ^0.8.0;
+library Address { function s() internal pure {} }
+==== Source: ERC20.sol ====
+pragma solidity ^0.8.0;
+
+import "./Address.sol";
+
+library SafeMath {
+    function sub(uint256 a, uint256 b) internal pure returns (uint256) {
+        return a - b;
+    }
+}
+
+contract ERC20 {
+    using SafeMath for uint256;
+    using Address for address;
+
+    mapping (address => uint256) private _balances;
+
+    function transferFrom(uint256 amount) public view {
+        _balances[msg.sender].sub(amount);
+    }
+}
+// ====
+// 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)\n    SafeMath.sub(0, 1) -- internal call