From d24302ace6832f7d957b6c599943bc769469c5dd Mon Sep 17 00:00:00 2001
From: Daniel Kirchner <daniel@ekpyron.org>
Date: Thu, 3 Dec 2020 13:00:30 +0100
Subject: [PATCH] Some fixes.

---
 libsmtutil/z3/Z3Loader.cpp | 15 ++++++++++++---
 libsolidity/formal/CHC.cpp |  4 ++--
 2 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/libsmtutil/z3/Z3Loader.cpp b/libsmtutil/z3/Z3Loader.cpp
index cf13e4d3381e..5538b2e01646 100644
--- a/libsmtutil/z3/Z3Loader.cpp
+++ b/libsmtutil/z3/Z3Loader.cpp
@@ -1,6 +1,8 @@
 #include <Z3Loader.h>
 #include <stdexcept>
 #include <z3.h>
+#include <z3_version.h>
+#include <iostream>
 
 Z3Loader const& Z3Loader::get()
 {
@@ -26,13 +28,20 @@ bool Z3Loader::available() const
 	unsigned build = 0;
 	unsigned rev = 0;
 	Z3_get_version(&major, &minor, &build, &rev);
-	return (major > 4 || (major == 4 && minor >= 6));
+	if (major != Z3_MAJOR_VERSION || minor != Z3_MINOR_VERSION || build != Z3_BUILD_NUMBER || rev != Z3_REVISION_NUMBER)
+		// TODO: proper warning, etc. - this function should probably return a BoolResult or something similar.
+		std::cerr << "Warning: solidity was build against Z3 "
+			<< Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER
+			<< " but version " << major << "." << minor << "." << build << "." << rev << " was found. Use at your own risk."
+			<< std::endl;
+	return (major == 4 && minor >= 6);
 }
 
-Z3Loader::Z3Loader(): m_handle(dlmopen(LM_ID_NEWLM, "libz3.so", RTLD_NOW))
+Z3Loader::Z3Loader(): m_handle(dlmopen(LM_ID_NEWLM, "libz3.so.4", RTLD_NOW))
 {
 }
 Z3Loader::~Z3Loader()
 {
-	dlclose(m_handle);
+	if (m_handle)
+		dlclose(m_handle);
 }
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index be3413770efa..3298deeb1c48 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -57,7 +57,7 @@ CHC::CHC(
 	m_enabledSolvers(_enabledSolvers),
 	m_queryTimeout(_timeout)
 {
-	bool usesZ3 = _enabledSolvers.z3;
+	bool usesZ3 = _enabledSolvers.z3 && Z3Interface::available();
 #ifndef HAVE_Z3
 	usesZ3 = false;
 #endif
@@ -734,7 +734,7 @@ void CHC::resetSourceAnalysis()
 
 	bool usesZ3 = false;
 #ifdef HAVE_Z3
-	usesZ3 = m_enabledSolvers.z3;
+	usesZ3 = m_enabledSolvers.z3 && Z3Interface::available();
 	if (usesZ3)
 	{
 		/// z3::fixedpoint does not have a reset mechanism, so we need to create another.