From e3ec22124eb3cdbe0f720682ff2dc202f63908fa Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Tue, 7 Apr 2020 01:09:03 +0200
Subject: [PATCH] [SMTChecker] Fix ICE in CHC internal calls

---
 Changelog.md                                  |  1 +
 libsolidity/formal/CHC.cpp                    |  6 ++++-
 .../functions/internal_call_inheritance.sol   | 20 ++++++++++++++++
 .../functions/internal_call_inheritance_2.sol | 24 +++++++++++++++++++
 4 files changed, 50 insertions(+), 1 deletion(-)
 create mode 100644 test/libsolidity/smtCheckerTests/functions/internal_call_inheritance.sol
 create mode 100644 test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol

diff --git a/Changelog.md b/Changelog.md
index 07be2d7ed..828d86ed4 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -7,6 +7,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix internal error in the CHC engine when calling inherited functions internally.
 
 
 
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index e10c16d39..5067e1396 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -961,7 +961,11 @@ smt::Expression CHC::predicate(FunctionCall const& _funCall)
 	for (auto const& var: function->returnParameters())
 		args.push_back(m_context.variable(*var)->currentValue());
 
-	return (*m_summaries.at(contract).at(function))(args);
+	if (contract->isLibrary())
+		return (*m_summaries.at(contract).at(function))(args);
+
+	solAssert(m_currentContract, "");
+	return (*m_summaries.at(m_currentContract).at(function))(args);
 }
 
 void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance.sol
new file mode 100644
index 000000000..5332dc590
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance.sol
@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function c() public pure returns (uint) { return 42; }
+}
+
+contract B is C {
+	function b() public pure returns (uint) { return c(); }
+}
+
+contract A is B {
+	uint public x;
+
+	function a() public {
+		x = b();
+		assert(x < 40);
+	}
+}
+// ----
+// Warning: (254-268): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol
new file mode 100644
index 000000000..262f0e498
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol
@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint y;
+	function c(uint _y) public returns (uint) {
+		y = _y;
+		return y;
+	}
+}
+
+contract B is C {
+	function b() public returns (uint) { return c(42); }
+}
+
+contract A is B {
+	uint public x;
+
+	function a() public {
+		x = b();
+		assert(x < 40);
+	}
+}
+// ----
+// Warning: (274-288): Assertion violation happens here