Add SMT tests.

4 files changed, 21 insertions, 7 deletions

diff --git a/docs/contributing.rst b/docs/contributing.rst
index 01caa5b1..0f7c3e72 100644
--- a/docs/contributing.rst
+++ b/docs/contributing.rst
@@ -64,9 +64,11 @@ Running the compiler tests
 ==========================
 
 Solidity includes different types of tests. They are included in the application
-called ``soltest``. Some of them require the ``cpp-ethereum`` client in testing mode.
+called ``soltest``. Some of them require the ``cpp-ethereum`` client in testing mode,
+some others require ``libz3`` to be installed.
 
-To run a subset of the tests that do not require ``cpp-ethereum``, use ``./build/test/soltest -- --no-ipc``.
+To disable the z3 tests, use ``./build/test/soltest -- --no-smt`` and
+to run a subset of the tests that do not require ``cpp-ethereum``, use ``./build/test/soltest -- --no-ipc``.
 
 For all other tests, you need to install `cpp-ethereum <https://github.com/ethereum/cpp-ethereum/releases/download/solidityTester/eth>`_ and run it in testing mode: ``eth --test -d /tmp/testeth``.
 
diff --git a/test/TestHelper.cpp b/test/TestHelper.cpp
index 094b59c6..c8747a06 100644
--- a/test/TestHelper.cpp
+++ b/test/TestHelper.cpp
@@ -45,6 +45,8 @@ Options::Options()
 			showMessages = true;
 		else if (string(suite.argv[i]) == "--no-ipc")
 			disableIPC = true;
+		else if (string(suite.argv[i]) == "--no-smt")
+			disableSMT = true;
 
 	if (!disableIPC && ipcPath.empty())
 		if (auto path = getenv("ETH_TEST_IPC"))
diff --git a/test/TestHelper.h b/test/TestHelper.h
index d50568ad..d25c5cd8 100644
--- a/test/TestHelper.h
+++ b/test/TestHelper.h
@@ -35,6 +35,7 @@ struct Options: boost::noncopyable
 	bool showMessages = false;
 	bool optimize = false;
 	bool disableIPC = false;
+	bool disableSMT = false;
 
 	static Options const& get();
 
diff --git a/test/boostTest.cpp b/test/boostTest.cpp
index d8c5b678..7b452e06 100644
--- a/test/boostTest.cpp
+++ b/test/boostTest.cpp
@@ -39,6 +39,17 @@
 
 using namespace boost::unit_test;
 
+namespace
+{
+void removeTestSuite(std::string const& _name)
+{
+	master_test_suite_t& master = framework::master_test_suite();
+	auto id = master.get(_name);
+	assert(id != INV_TEST_UNIT_ID);
+	master.remove(id);
+}
+}
+
 test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] )
 {
 	master_test_suite_t& master = framework::master_test_suite();
@@ -57,12 +68,10 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] )
 			"SolidityEndToEndTest",
 			"SolidityOptimizer"
 		})
-		{
-			auto id = master.get(suite);
-			assert(id != INV_TEST_UNIT_ID);
-			master.remove(id);
-		}
+			removeTestSuite(suite);
 	}
+	if (dev::test::Options::get().disableSMT)
+		removeTestSuite("SMTChecker");
 
 	return 0;
 }