Prepare build system for Z3.

libsolidity/CMakeLists.txt

@@ -2,5 +2,19 @@
 file(GLOB_RECURSE sources "*.cpp" "../libjulia/*.cpp")
 file(GLOB_RECURSE headers "*.h" "../libjulia/*.h")
 
+find_package(Z3 QUIET)
+if (${Z3_FOUND})
+  include_directories(${Z3_INCLUDE_DIR})
+  add_definitions(-DHAVE_Z3)
+  message("Z3 SMT solver FOUND.")
+else()
+  message("Z3 SMT solver NOT found.")
+  list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/Z3Interface.cpp")
+endif()
+
 add_library(solidity ${sources} ${headers})
-target_link_libraries(solidity PUBLIC evmasm devcore z3)
+target_link_libraries(solidity PUBLIC evmasm devcore)
+
+if (${Z3_FOUND})
+  target_link_libraries(solidity PUBLIC ${Z3_LIBRARY})
+endif()

libsolidity/formal/SMTChecker.cpp

@@ -76,6 +76,9 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 void SMTChecker::endVisit(FunctionDefinition const&)
 {
 	// TOOD we could check for "reachability", i.e. satisfiability here.
+	// We only handle local variables, so we clear everything.
+	// If we add storage variables, those should be cleared differently.
+	m_currentSequenceCounter.clear();
 	m_interface.pop();
 	m_currentFunction = nullptr;
 }