diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index cdfbad3ce..a25f3a1bb 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -775,8 +775,13 @@ void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)
 	auto const& args = _funCall.sortedArguments();
 	auto argsActualLength = kind == FunctionType::Kind::ABIDecode ? 1 : args.size();
 
-	vector<smtutil::Expression> symbArgs;
 	solAssert(inTypes.size() == argsActualLength, "");
+	if (argsActualLength == 0)
+	{
+		defineExpr(_funCall, smt::zeroValue(TypeProvider::bytesMemory()));
+		return;
+	}
+	vector<smtutil::Expression> symbArgs;
 	for (unsigned i = 0; i < argsActualLength; ++i)
 		if (args.at(i))
 			symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i)));
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_no_arguments.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_no_arguments.sol
new file mode 100644
index 000000000..bdc95c9c6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_no_arguments.sol
@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() pure public {
+		bytes memory res = abi.encode();
+		assert(res.length == 0); // should hold
+		assert(res.length > 0); // should fail
+		res = abi.encodePacked();
+		assert(res.length == 0); // should hold
+		assert(res.length > 0); // should fail
+		res = abi.encodeWithSelector(0);
+		assert(res.length == 4); // should hold, but SMTChecker cannot know this yet
+		res = abi.encodeWithSignature("");
+		assert(res.length == 4); // should hold, but SMTChecker cannot know this yet
+	}
+}
+// ----
+// Warning 6328: (152-174): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (263-285): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (339-362): CHC: Assertion violation happens here.
+// Warning 6328: (455-478): CHC: Assertion violation happens here.