diff --git a/Changelog.md b/Changelog.md
index 32d3db1d4..b4a833463 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -15,6 +15,7 @@ Compiler Features:
 Bugfixes:
  * Code generator: Do not pad empty string literals with a single 32-byte zero field in the ABI coder v1.
  * SMTChecker: Fix internal compiler error when doing bitwise compound assignment with string literals.
+ * SMTChecker: Fix internal error when trying to generate counterexamples with old z3.
  * Yul Optimizer: Fix a bug in NameSimplifier where a new name created by NameSimplifier could also be created by NameDispenser.
  * Yul Optimizer: Removed NameSimplifier from optimization steps available to users.
 
diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp
index 66ba55801..1196b27ff 100644
--- a/libsmtutil/Z3CHCInterface.cpp
+++ b/libsmtutil/Z3CHCInterface.cpp
@@ -33,6 +33,13 @@ Z3CHCInterface::Z3CHCInterface(optional<unsigned> _queryTimeout):
 	m_context(m_z3Interface->context()),
 	m_solver(*m_context)
 {
+	Z3_get_version(
+		&get<0>(m_version),
+		&get<1>(m_version),
+		&get<2>(m_version),
+		&get<3>(m_version)
+	);
+
 	// These need to be set globally.
 	z3::set_param("rewriter.pull_cheap_ite", true);
 
@@ -73,7 +80,6 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name)
 pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
 {
 	CheckResult result;
-	CHCSolverInterface::CexGraph cex;
 	try
 	{
 		z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr);
@@ -82,9 +88,14 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
 		case z3::check_result::sat:
 		{
 			result = CheckResult::SATISFIABLE;
-			auto proof = m_solver.get_answer();
-			auto cex = cexGraph(proof);
-			return {result, cex};
+			// z3 version 4.8.8 modified Spacer to also return
+			// proofs containing nonlinear clauses.
+			if (m_version >= tuple(4, 8, 8, 0))
+			{
+				auto proof = m_solver.get_answer();
+				return {result, cexGraph(proof)};
+			}
+			break;
 		}
 		case z3::check_result::unsat:
 		{
@@ -112,10 +123,9 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
 			result = CheckResult::UNKNOWN;
 		else
 			result = CheckResult::ERROR;
-		cex = {};
 	}
 
-	return {result, cex};
+	return {result, {}};
 }
 
 void Z3CHCInterface::setSpacerOptions(bool _preProcessing)
diff --git a/libsmtutil/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h
index a0d678536..a0e4bfa67 100644
--- a/libsmtutil/Z3CHCInterface.h
+++ b/libsmtutil/Z3CHCInterface.h
@@ -25,6 +25,7 @@
 #include <libsmtutil/CHCSolverInterface.h>
 #include <libsmtutil/Z3Interface.h>
 
+#include <tuple>
 #include <vector>
 
 namespace solidity::smtutil
@@ -64,6 +65,8 @@ private:
 	z3::context* m_context;
 	// Horn solver.
 	z3::fixedpoint m_solver;
+
+	std::tuple<unsigned, unsigned, unsigned, unsigned> m_version = std::tuple(0, 0, 0, 0);
 };
 
 }