Fix SMTChecker bug when a public library function is called internally by an internal library function, which in turn is called internally by a contract.

test/libsolidity/SMTCheckerTest.cpp

@@ -29,6 +29,10 @@ using namespace solidity::frontend::test;
 
 SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, EVMVersion{})
 {
+	auto contract = m_reader.stringSetting("SMTContract", "");
+	if (!contract.empty())
+		m_modelCheckerSettings.contracts.contracts[""] = {contract};
+
 	auto const& showUnproved = m_reader.stringSetting("SMTShowUnproved", "yes");
 	if (showUnproved == "no")
 		m_modelCheckerSettings.showUnproved = false;

test/libsolidity/smtCheckerTests/functions/library_public_called_as_internal_1.sol

@@ -0,0 +1,26 @@
+library L {
+    function f1(uint x) public pure {
+        assert(x > 0); // should fail
+    }
+    function f(uint x) internal pure { f1(x); }
+}
+
+contract C {
+    function g(uint x) external pure {
+        // This should trigger the assertion failure
+        // since it calls `f` internally, which calls
+        // `f1` internally.
+        return L.f(x);
+    }
+
+    function h(uint x) external pure {
+        // This should not trigger the assertion failure
+        // since it delegatecalls and that's not supported.
+        return L.f1(x);
+    }
+}
+// ====
+// SMTContract: C
+// ----
+// Warning 4588: (533-540): Assertion checker does not yet implement this type of function call.
+// Warning 6328: (58-71): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    L.f(0) -- internal call\n        L.f1(0) -- internal call

test/libsolidity/smtCheckerTests/functions/library_public_called_as_internal_2.sol

@@ -0,0 +1,24 @@
+library L {
+    function f1(uint x) public pure {
+        assert(x > 0); // should fail
+    }
+    function f() internal pure {
+        f1(0); // should cause the assertion in `f1` to fail
+    }
+    function g() internal pure {
+        f1(1); // should not cause the assertion in `f1` to fail
+    }
+}
+
+contract C {
+    function f() external pure {
+        return L.f(); // should cause the assertion to fail
+    }
+    function g() external pure {
+        return L.g(); // should not cause the assertion to fail
+    }
+}
+// ====
+// SMTContract: C
+// ----
+// Warning 6328: (58-71): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n    L.f() -- internal call\n        L.f1(0) -- internal call