Merge pull request #7894 from ethereum/smt_isoltest_choice

[SMTChecker] Create SMTSolver option in isoltest
2023-10-03 13:03:40 +00:00 · 2019-12-09 16:41:20 +01:00
parent 5404343dd6 beed0f6a27
commit 2579a12bb8
94 changed files with 534 additions and 282 deletions
@@ -153,19 +153,6 @@ do \
 } \
 while(0)

-#define CHECK_SUCCESS_OR_WARNING(text, substring) \
-do \
-{ \
-	auto sourceAndError = parseAnalyseAndReturnError((text), true); \
-	auto const& errors = sourceAndError.second; \
-	if (!errors.empty()) \
-	{ \
-		auto message = searchErrors(errors, {{(Error::Type::Warning), (substring)}}); \
-		BOOST_CHECK_MESSAGE(message.empty(), message); \
-	} \
-} \
-while(0)
-
 }
 }
 }
@@ -59,198 +59,6 @@ protected:

 BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework)

-BOOST_AUTO_TEST_CASE(division)
-{
-	string text = R"(
-		contract C {
-			function f(uint x, uint y) public pure returns (uint) {
-				return x / y;
-			}
-		}
-	)";
-	CHECK_WARNING(text, "Division by zero");
-	text = R"(
-		contract C {
-			function f(uint x, uint y) public pure returns (uint) {
-				require(y != 0);
-				return x / y;
-			}
-		}
-	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
-	text = R"(
-		contract C {
-			function f(int x, int y) public pure returns (int) {
-				require(y != 0);
-				return x / y;
-			}
-		}
-	)";
-	CHECK_WARNING(text, "Overflow");
-	text = R"(
-		contract C {
-			function f(int x, int y) public pure returns (int) {
-				require(y != 0);
-				require(y != -1);
-				return x / y;
-			}
-		}
-	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
-	text = R"(
-		contract C {
-			function mul(uint256 a, uint256 b) internal pure returns (uint256) {
-				uint256 c;
-				if (a != 0) {
-					c = a * b;
-					require(c / a == b);
-				}
-				return c;
-			}
-		}
-	)";
-	CHECK_SUCCESS_OR_WARNING(text, "might happen");
-	text = R"(
-		contract C {
-			function mul(uint256 a, uint256 b) internal pure returns (uint256) {
-				if (a == 0) {
-					return 0;
-				}
-				// TODO remove when SMTChecker sees that this code is the `else` of the `return`.
-				require(a != 0);
-				uint256 c = a * b;
-				require(c / a == b);
-				return c;
-			}
-		}
-	)";
-	CHECK_SUCCESS_OR_WARNING(text, "might happen");
-	text = R"(
-		contract C {
-			function div(uint256 a, uint256 b) internal pure returns (uint256) {
-				require(b > 0);
-				uint256 c = a / b;
-				return c;
-			}
-		}
-	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
-
-
-}
-
-BOOST_AUTO_TEST_CASE(division_truncates_correctly)
-{
-	string text = R"(
-		contract C {
-			function f(uint x, uint y) public pure {
-				x = 7;
-				y = 2;
-				assert(x / y == 3);
-			}
-		}
-	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
-	text = R"(
-		contract C {
-			function f(int x, int y) public pure {
-				x = 7;
-				y = 2;
-				assert(x / y == 3);
-			}
-		}
-	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
-	text = R"(
-		contract C {
-			function f(int x, int y) public pure {
-				x = -7;
-				y = 2;
-				assert(x / y == -3);
-			}
-		}
-	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
-	text = R"(
-		contract C {
-			function f(int x, int y) public pure {
-				x = 7;
-				y = -2;
-				assert(x / y == -3);
-			}
-		}
-	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
-	text = R"(
-		contract C {
-			function f(int x, int y) public pure {
-				x = -7;
-				y = -2;
-				assert(x / y == 3);
-			}
-		}
-	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
-}
-
-BOOST_AUTO_TEST_CASE(compound_assignment_division)
-{
-	string text = R"(
-		contract C {
-			function f(uint x) public pure {
-				require(x == 2);
-				uint y = 10;
-				y /= y / x;
-				assert(y == x);
-				assert(y == 0);
-			}
-		}
-	)";
-	CHECK_WARNING(text, "Assertion violation");
-	text = R"(
-		contract C {
-			uint[] array;
-			function f(uint x, uint p) public {
-				require(x == 2);
-				array[p] = 10;
-				array[p] /= array[p] / x;
-				assert(array[p] == x);
-				assert(array[p] == 0);
-			}
-		}
-	)";
-	CHECK_WARNING(text, "Assertion violation");
-	text = R"(
-		contract C {
-			mapping (uint => uint) map;
-			function f(uint x, uint p) public {
-				require(x == 2);
-				map[p] = 10;
-				map[p] /= map[p] / x;
-				assert(map[p] == x);
-				assert(map[p] == 0);
-			}
-		}
-	)";
-	CHECK_WARNING(text, "Assertion violation");
-}
-
-BOOST_AUTO_TEST_CASE(mod)
-{
-	string text = R"(
-		contract C {
-			function f(int x, int y) public pure {
-				require(y == -10);
-				require(x == 100);
-				int z1 = x % y;
-				int z2 = x % -y;
-				assert(z1 == z2);
-			}
-		}
-	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
-}
-
 BOOST_AUTO_TEST_CASE(import_base)
 {
 	CompilerStack c;
@@ -36,7 +36,7 @@ using namespace dev;
 using namespace std;
 using namespace boost::unit_test;

-SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _evmVersion)
+SMTCheckerJSONTest::SMTCheckerJSONTest(string const& _filename, langutil::EVMVersion _evmVersion)
 : SyntaxTest(_filename, _evmVersion)
 {
 	if (!boost::algorithm::ends_with(_filename, ".sol"))
@@ -50,7 +50,7 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _ev
 		BOOST_THROW_EXCEPTION(runtime_error("Invalid JSON file."));
 }

-TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
+TestCase::TestResult SMTCheckerJSONTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
 {
 	StandardCompiler compiler;

@@ -129,7 +129,7 @@ TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePr
 	return printExpectationAndError(_stream, _linePrefix, _formatted) ? TestResult::Success : TestResult::Failure;
 }

-vector<string> SMTCheckerTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib)
+vector<string> SMTCheckerJSONTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib)
 {
 	vector<string> hashes;
 	Json::Value const& auxInputs = _jsonObj[_auxInput];
@@ -143,7 +143,7 @@ vector<string> SMTCheckerTest::hashesFromJson(Json::Value const& _jsonObj, strin
 	return hashes;
 }

-Json::Value SMTCheckerTest::buildJson(string const& _extra)
+Json::Value SMTCheckerJSONTest::buildJson(string const& _extra)
 {
 	string language = "\"language\": \"Solidity\"";
 	string sources = " \"sources\": { ";
@@ -30,14 +30,14 @@ namespace solidity
 namespace test
 {

-class SMTCheckerTest: public SyntaxTest
+class SMTCheckerJSONTest: public SyntaxTest
 {
 public:
 	static std::unique_ptr<TestCase> create(Config const& _config)
 	{
-		return std::make_unique<SMTCheckerTest>(_config.filename, _config.evmVersion);
+		return std::make_unique<SMTCheckerJSONTest>(_config.filename, _config.evmVersion);
 	}
-	SMTCheckerTest(std::string const& _filename, langutil::EVMVersion _evmVersion);
+	SMTCheckerJSONTest(std::string const& _filename, langutil::EVMVersion _evmVersion);

 	TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override;

@@ -0,0 +1,71 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <test/libsolidity/SMTCheckerTest.h>
+#include <test/Options.h>
+
+#include <libsolidity/formal/ModelChecker.h>
+
+using namespace langutil;
+using namespace dev::solidity;
+using namespace dev::solidity::test;
+using namespace dev;
+using namespace std;
+
+SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _evmVersion): SyntaxTest(_filename, _evmVersion)
+{
+	if (m_settings.count("SMTSolvers"))
+	{
+		auto const& choice = m_settings.at("SMTSolvers");
+		if (choice == "any")
+			m_enabledSolvers = smt::SMTSolverChoice::All();
+		else if (choice == "z3")
+			m_enabledSolvers = smt::SMTSolverChoice::Z3();
+		else if (choice == "cvc4")
+			m_enabledSolvers = smt::SMTSolverChoice::CVC4();
+		else if (choice == "none")
+			m_enabledSolvers = smt::SMTSolverChoice::None();
+		else
+			BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT solver choice."));
+	}
+	else
+		m_enabledSolvers = smt::SMTSolverChoice::All();
+}
+
+TestCase::TestResult SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
+{
+	setupCompiler();
+	compiler().setSMTSolverChoice(m_enabledSolvers);
+	parseAndAnalyze();
+	filterObtainedErrors();
+
+	return printExpectationAndError(_stream, _linePrefix, _formatted) ? TestResult::Success : TestResult::Failure;
+}
+
+bool SMTCheckerTest::validateSettings(langutil::EVMVersion _evmVersion)
+{
+	auto available = ModelChecker::availableSolvers();
+	if (!available.z3)
+		m_enabledSolvers.z3 = false;
+	if (!available.cvc4)
+		m_enabledSolvers.cvc4 = false;
+
+	if (m_enabledSolvers.none())
+		return false;
+
+	return SyntaxTest::validateSettings(_evmVersion);
+}
@@ -0,0 +1,55 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <test/libsolidity/SyntaxTest.h>
+
+#include <libsolidity/formal/SolverInterface.h>
+
+#include <string>
+
+namespace dev
+{
+namespace solidity
+{
+namespace test
+{
+
+class SMTCheckerTest: public SyntaxTest
+{
+public:
+	static std::unique_ptr<TestCase> create(Config const& _config)
+	{
+		return std::make_unique<SMTCheckerTest>(_config.filename, _config.evmVersion);
+	}
+	SMTCheckerTest(std::string const& _filename, langutil::EVMVersion _evmVersion);
+
+	TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override;
+
+	bool validateSettings(langutil::EVMVersion _evmVersion) override;
+
+protected:
+	/// This is set via option SMTSolvers in the test.
+	/// The possible options are `all`, `z3`, `cvc4`, `none`,
+	/// where if none is given the default used option is `all`.
+	smt::SMTSolverChoice m_enabledSolvers;
+};
+
+}
+}
+}
@@ -73,59 +73,9 @@ SyntaxTest::SyntaxTest(string const& _filename, langutil::EVMVersion _evmVersion

 TestCase::TestResult SyntaxTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
 {
-	string const versionPragma = "pragma solidity >=0.0;\n";
-	compiler().reset();
-	auto sourcesWithPragma = m_sources;
-	for (auto& source: sourcesWithPragma)
-		source.second = versionPragma + source.second;
-	compiler().setSources(sourcesWithPragma);
-	compiler().setEVMVersion(m_evmVersion);
-	compiler().setParserErrorRecovery(m_parserErrorRecovery);
-	compiler().setOptimiserSettings(
-		m_optimiseYul ?
-		OptimiserSettings::full() :
-		OptimiserSettings::minimal()
-	);
-	if (compiler().parse())
-		if (compiler().analyze())
-			try
-			{
-				if (!compiler().compile())
-					BOOST_THROW_EXCEPTION(runtime_error("Compilation failed even though analysis was successful."));
-			}
-			catch (UnimplementedFeatureError const& _e)
-			{
-				m_errorList.emplace_back(SyntaxTestError{
-					"UnimplementedFeatureError",
-					errorMessage(_e),
-					"",
-					-1,
-					-1
-				});
-			}
-
-	for (auto const& currentError: filterErrors(compiler().errors(), true))
-	{
-		int locationStart = -1, locationEnd = -1;
-		string sourceName;
-		if (auto location = boost::get_error_info<errinfo_sourceLocation>(*currentError))
-		{
-			// ignore the version pragma inserted by the testing tool when calculating locations.
-			if (location->start >= static_cast<int>(versionPragma.size()))
-				locationStart = location->start - versionPragma.size();
-			if (location->end >= static_cast<int>(versionPragma.size()))
-				locationEnd = location->end - versionPragma.size();
-			if (location->source)
-				sourceName = location->source->name();
-		}
-		m_errorList.emplace_back(SyntaxTestError{
-			currentError->typeName(),
-			errorMessage(*currentError),
-			sourceName,
-			locationStart,
-			locationEnd
-		});
-	}
+	setupCompiler();
+	parseAndAnalyze();
+	filterObtainedErrors();

 	return printExpectationAndError(_stream, _linePrefix, _formatted) ? TestResult::Success : TestResult::Failure;
 }
@@ -207,6 +157,70 @@ void SyntaxTest::printSource(ostream& _stream, string const& _linePrefix, bool _
 		}
 }

+void SyntaxTest::setupCompiler()
+{
+	string const versionPragma = "pragma solidity >=0.0;\n";
+	compiler().reset();
+	auto sourcesWithPragma = m_sources;
+	for (auto& source: sourcesWithPragma)
+		source.second = versionPragma + source.second;
+	compiler().setSources(sourcesWithPragma);
+	compiler().setEVMVersion(m_evmVersion);
+	compiler().setParserErrorRecovery(m_parserErrorRecovery);
+	compiler().setOptimiserSettings(
+		m_optimiseYul ?
+		OptimiserSettings::full() :
+		OptimiserSettings::minimal()
+	);
+}
+
+void SyntaxTest::parseAndAnalyze()
+{
+	if (compiler().parse() && compiler().analyze())
+		try
+		{
+			if (!compiler().compile())
+				BOOST_THROW_EXCEPTION(runtime_error("Compilation failed even though analysis was successful."));
+		}
+		catch (UnimplementedFeatureError const& _e)
+		{
+			m_errorList.emplace_back(SyntaxTestError{
+				"UnimplementedFeatureError",
+				errorMessage(_e),
+				"",
+				-1,
+				-1
+			});
+		}
+}
+
+void SyntaxTest::filterObtainedErrors()
+{
+	string const versionPragma = "pragma solidity >=0.0;\n";
+	for (auto const& currentError: filterErrors(compiler().errors(), true))
+	{
+		int locationStart = -1, locationEnd = -1;
+		string sourceName;
+		if (auto location = boost::get_error_info<errinfo_sourceLocation>(*currentError))
+		{
+			// ignore the version pragma inserted by the testing tool when calculating locations.
+			if (location->start >= static_cast<int>(versionPragma.size()))
+				locationStart = location->start - versionPragma.size();
+			if (location->end >= static_cast<int>(versionPragma.size()))
+				locationEnd = location->end - versionPragma.size();
+			if (location->source)
+				sourceName = location->source->name();
+		}
+		m_errorList.emplace_back(SyntaxTestError{
+			currentError->typeName(),
+			errorMessage(*currentError),
+			sourceName,
+			locationStart,
+			locationEnd
+		});
+	}
+}
+
 void SyntaxTest::printErrorList(
 	ostream& _stream,
 	vector<SyntaxTestError> const& _errorList,
@@ -52,7 +52,7 @@ struct SyntaxTestError
 };


-class SyntaxTest: AnalysisFramework, public EVMVersionRestrictedTestCase
+class SyntaxTest: public AnalysisFramework, public EVMVersionRestrictedTestCase
 {
 public:
 	static std::unique_ptr<TestCase> create(Config const& _config)
@@ -76,6 +76,10 @@ public:

 	static std::string errorMessage(Exception const& _e);
 protected:
+	void setupCompiler();
+	void parseAndAnalyze();
+	void filterObtainedErrors();
+
 	static void printErrorList(
 		std::ostream& _stream,
 		std::vector<SyntaxTestError> const& _errors,
@@ -14,3 +14,5 @@ contract C is B {
 		assert(x == 2);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -18,3 +18,5 @@ contract C is B {
 		assert(x == 0);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -9,3 +9,5 @@ contract Simple {
 		assert(y == x);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -7,4 +7,5 @@ contract Simple {
 		assert(y == x);
 	}
 }
-// ----
+// ====
+// SMTSolvers: z3
@@ -15,3 +15,5 @@ contract Simple {
 		assert(y == x);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -12,3 +12,5 @@ contract Simple {
 		assert(y == x);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -30,3 +30,5 @@ contract C {
 		assert(x < 9);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -28,5 +28,7 @@ contract C {
 		assert(x < 2);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (311-324): Assertion violation happens here
@@ -11,6 +11,8 @@ contract C
 		assert(x < 14);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (179-193): Assertion violation happens here
@@ -13,5 +13,7 @@ contract C
 		assert(x > 0);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here
@@ -10,6 +10,8 @@ contract C {
 		assert(x == 0);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (104-109): Unreachable code.
 // Warning: (122-128): Unreachable code.
@@ -14,6 +14,8 @@ contract C {
 		assert(a == 1);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (128-133): Unreachable code.
 // Warning: (147-151): Unreachable code.
@@ -14,6 +14,8 @@ contract C {
 		assert(a == 2);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (128-133): Unreachable code.
 // Warning: (147-151): Unreachable code.
@@ -10,6 +10,8 @@ contract C {
 		assert(x == 1);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (104-109): Unreachable code.
 // Warning: (122-128): Unreachable code.
@@ -10,5 +10,7 @@ contract C {
 		assert(x == 0);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (107-112): Unreachable code.
@@ -15,3 +15,5 @@ contract C
 		assert(x >= 10);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -14,5 +14,7 @@ contract C
 		assert(x >= 10);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (201-216): Assertion violation happens here
@@ -13,3 +13,5 @@ contract C
 		assert(x > 0);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -14,5 +14,7 @@ contract C
 		assert(x > 15);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (185-199): Assertion violation happens here
@@ -11,6 +11,8 @@ contract C
 		assert(x < 14);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
 // Warning: (189-203): Assertion violation happens here
@@ -13,6 +13,8 @@ contract C
 		assert(x > 0);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (296-309): Error trying to invoke SMT solver.
 // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
@@ -8,5 +8,7 @@ contract C
 		assert(x == 0);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (102-105): Unreachable code.
@@ -6,3 +6,5 @@ contract C {
        assert(x == 2);
    }
 }
+// ====
+// SMTSolvers: z3
@@ -6,3 +6,5 @@ contract C {
        }
    }
 }
+// ====
+// SMTSolvers: z3
@@ -6,3 +6,5 @@ contract C {
        }
    }
 }
+// ====
+// SMTSolvers: z3
@@ -6,5 +6,7 @@ contract C {
        }
    }
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (136-150): Assertion violation happens here
@@ -8,5 +8,7 @@ contract C {
        assert(y == 3);
    }
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (167-181): Assertion violation happens here
@@ -9,4 +9,5 @@ contract C {
        assert(y < 4);
    }
 }
-// ----
+// ====
+// SMTSolvers: z3
@@ -14,6 +14,8 @@ contract LoopFor2 {
 		assert(b[0] == 900);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (281-301): Assertion violation happens here
 // Warning: (305-324): Assertion violation happens here
@@ -16,6 +16,8 @@ contract LoopFor2 {
 		assert(b[0] == 900);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (274-294): Assertion violation happens here
 // Warning: (321-340): Assertion violation happens here
@@ -17,5 +17,7 @@ contract LoopFor2 {
 		assert(b[0] == 900);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (312-331): Assertion violation happens here
@@ -17,6 +17,8 @@ contract LoopFor2 {
 		assert(b[0] == 900);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (290-309): Assertion violation happens here
 // Warning: (313-332): Assertion violation happens here
@@ -6,5 +6,7 @@ contract C {
        assert(x == 2);
    }
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (122-128): Condition is always true.
@@ -9,5 +9,7 @@ contract C {
        assert(x == 2);
    }
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (138-144): Condition is always true.
@@ -13,5 +13,7 @@ contract C {
        assert(x == 2);
    }
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (115-121): Unused local variable.
@@ -6,5 +6,7 @@ contract C {
        assert(x == 2);
    }
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (122-127): Condition is always false.
@@ -13,4 +13,6 @@ contract C
 		assert(x > 0);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
@@ -15,3 +15,5 @@ contract C
 		assert(x >= 10);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -15,5 +15,7 @@ contract C
 		assert(x >= 10);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (218-233): Assertion violation happens here
@@ -14,3 +14,5 @@ contract C
 		assert(x >= 10);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -17,6 +17,8 @@ contract C
 		assert(x >= 17);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (169-176): Unreachable code.
 // Warning: (227-242): Assertion violation happens here
@@ -10,5 +10,7 @@ contract C
 		assert(x < 14);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (139-153): Assertion violation happens here
@@ -18,4 +18,5 @@ contract C
 		assert(x > 0);
 	}
 }
-// ----
+// ====
+// SMTSolvers: z3
@@ -11,3 +11,5 @@ contract C {
 		assert(x < 2);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -12,5 +12,7 @@ contract C
 		assert(x == 1);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (128-131): Unreachable code.
@@ -11,6 +11,8 @@ contract C
 		assert(x == 2);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (120-123): Unreachable code.
 // Warning: (131-145): Assertion violation happens here
@@ -11,4 +11,6 @@ contract C {
 		assert(x == 2);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
@@ -9,5 +9,7 @@ contract C
 		assert(x == 0);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (98-104): Condition is always true.
@@ -16,6 +16,8 @@ contract LoopFor2 {
 		assert(b[0] == 900);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (281-301): Assertion violation happens here
 // Warning: (305-324): Assertion violation happens here
@@ -20,6 +20,8 @@ contract LoopFor2 {
 		assert(b[0] == 900);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (362-382): Assertion violation happens here
 // Warning: (409-428): Assertion violation happens here
@@ -9,5 +9,7 @@ contract C {
        assert(x == 2);
    }
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (194-208): Assertion violation happens here
@@ -7,3 +7,5 @@ contract C {
        }
    }
 }
+// ====
+// SMTSolvers: z3
@@ -7,5 +7,7 @@ contract C {
        assert(x == 2);
    }
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (187-201): Assertion violation happens here
@@ -7,4 +7,5 @@ contract C {
        assert(x != 2);
    }
 }
-// ----
+// ====
+// SMTSolvers: z3
@@ -8,5 +8,7 @@ contract C {
        assert(x == 7);
    }
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (216-230): Assertion violation happens here
@@ -28,3 +28,5 @@ contract C
 		assert(x >= 15);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -28,6 +28,8 @@ contract C
 		assert(x >= 20);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (329-344): Assertion violation happens here
 // Warning: (380-395): Assertion violation happens here
@@ -26,3 +26,5 @@ contract C
 		assert(x >= 15);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -26,6 +26,8 @@ contract C
 		assert(x >= 20);
 	}
 }
+// ====
+// SMTSolvers: z3
 // ----
 // Warning: (323-338): Assertion violation happens here
 // Warning: (362-377): Assertion violation happens here
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x) public pure {
+		require(x == 2);
+		uint y = 10;
+		y /= y / x;
+		assert(y == x);
+		assert(y == 0);
+	}
+}
+// ----
+// Warning: (147-161): Assertion violation happens here
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+	uint[] array;
+	function f(uint x, uint p) public {
+		require(x == 2);
+		array[p] = 10;
+		array[p] /= array[p] / x;
+		assert(array[p] == x);
+		assert(array[p] == 0);
+	}
+}
+// ----
+// Warning: (188-209): Assertion violation happens here
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+	mapping (uint => uint) map;
+	function f(uint x, uint p) public {
+		require(x == 2);
+		map[p] = 10;
+		map[p] /= map[p] / x;
+		assert(map[p] == x);
+		assert(map[p] == 0);
+	}
+}
+// ----
+// Warning: (194-213): Assertion violation happens here
@@ -13,3 +13,5 @@ contract C
 		assert(a[1][1] == 0);
 	}
 }
+// ====
+// SMTSolvers: z3
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x, uint y) public pure returns (uint) {
+		return x / y;
+	}
+}
+// ----
+// Warning: (111-116): Division by zero happens here
@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x, uint y) public pure returns (uint) {
+		require(y != 0);
+		return x / y;
+	}
+}
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(int x, int y) public pure returns (int) {
+		require(y != 0);
+		return x / y;
+	}
+}
+// ----
+// Warning: (127-132): Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(int x, int y) public pure returns (int) {
+		require(y != 0);
+		require(y != -1);
+		return x / y;
+	}
+}
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract C {
+	function mul(uint256 a, uint256 b) internal pure returns (uint256) {
+		uint256 c;
+		if (a != 0) {
+			c = a * b;
+			require(c / a == b);
+		}
+		return c;
+	}
+}
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+	function mul(uint256 a, uint256 b) internal pure returns (uint256) {
+		if (a == 0) {
+			return 0;
+		}
+		// TODO remove when SMTChecker sees that this code is the `else` of the `return`.
+		require(a != 0);
+		uint256 c = a * b;
+		require(c / a == b);
+		return c;
+	}
+}
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+	function div(uint256 a, uint256 b) internal pure returns (uint256) {
+		require(b > 0);
+		uint256 c = a / b;
+		return c;
+	}
+}
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(uint x, uint y) public pure {
+		x = 7;
+		y = 2;
+		assert(x / y == 3);
+	}
+}
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(int x, int y) public pure {
+		x = 7;
+		y = 2;
+		assert(x / y == 3);
+	}
+}
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(int x, int y) public pure {
+		x = -7;
+		y = 2;
+		assert(x / y == -3);
+	}
+}
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(int x, int y) public pure {
+		x = 7;
+		y = -2;
+		assert(x / y == -3);
+	}
+}
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(int x, int y) public pure {
+		x = -7;
+		y = -2;
+		assert(x / y == 3);
+	}
+}
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract C {
+	function f(int x, int y) public pure {
+		require(y == -10);
+		require(x == 100);
+		int z1 = x % y;
+		int z2 = x % -y;
+		assert(z1 == z2);
+	}
+}
@@ -8,4 +8,5 @@ contract C
 		assert(x != map[x]);
 	}
 }
-// ----
+// ====
+// SMTSolvers: z3