From 75663dc91e58f59d252cdba9ff4772d1497412aa Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 1 Jul 2019 16:11:29 +0200
Subject: [PATCH] [SMTChecker] Fix require with message

---
 libsolidity/formal/BMC.cpp                             |  2 +-
 libsolidity/formal/SMTEncoder.cpp                      | 10 +++++-----
 .../simple_assert_with_require_message.sol             |  9 +++++++++
 3 files changed, 15 insertions(+), 6 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/verification_target/simple_assert_with_require_message.sol

diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index a691e2e9f..26d48b5d6 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -386,7 +386,7 @@ void BMC::visitAssert(FunctionCall const& _funCall)
 void BMC::visitRequire(FunctionCall const& _funCall)
 {
 	auto const& args = _funCall.arguments();
-	solAssert(args.size() == 1, "");
+	solAssert(args.size() >= 1, "");
 	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
 	if (isRootFunction())
 		addVerificationTarget(
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 30aa95226..95d874292 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -501,16 +501,16 @@ void SMTEncoder::visitAssert(FunctionCall const& _funCall)
 {
 	auto const& args = _funCall.arguments();
 	solAssert(args.size() == 1, "");
-	solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
-	addPathImpliedExpression(expr(*args[0]));
+	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
+	addPathImpliedExpression(expr(*args.front()));
 }
 
 void SMTEncoder::visitRequire(FunctionCall const& _funCall)
 {
 	auto const& args = _funCall.arguments();
-	solAssert(args.size() == 1, "");
-	solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
-	addPathImpliedExpression(expr(*args[0]));
+	solAssert(args.size() >= 1, "");
+	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
+	addPathImpliedExpression(expr(*args.front()));
 }
 
 void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
diff --git a/test/libsolidity/smtCheckerTests/verification_target/simple_assert_with_require_message.sol b/test/libsolidity/smtCheckerTests/verification_target/simple_assert_with_require_message.sol
new file mode 100644
index 000000000..bf77fe015
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/verification_target/simple_assert_with_require_message.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint a) public pure {
+		require(a < 10, "Input number is too large.");
+		assert(a < 20);
+	}
+}
+// ----
+// Warning: (97-125): Assertion checker does not yet support the type of this literal (literal_string "Input number is too large.").