Merge pull request #5189 from ethereum/smt_function_call

[SMTChecker] Inline calls to internal functions

1 files changed, 17 insertions, 0 deletions

diff --git a/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol
new file mode 100644
index 00000000..d2f8ab1d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_recursive.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function g() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			g();
+		}
+		else
+			assert(a == 0);
+	}
+}
+
+// ----
+// Warning: (111-114): Assertion checker does not support recursive function calls.