From 3a01b432c4083b0a168aa8314281721780961558 Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@gmail.com>
Date: Fri, 11 Aug 2023 12:44:34 +0200
Subject: [PATCH] Hack to get around problem in Z3

---
 libsolidity/formal/SymbolicTypes.cpp | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 45b872b3d..ad001e8e5 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -23,12 +23,24 @@
 #include <libsolidity/ast/TypeProvider.h>
 #include <libsolidity/ast/Types.h>
 #include <libsolutil/CommonData.h>
+#include <algorithm>
 #include <memory>
 #include <vector>
 
 using namespace solidity::util;
 using namespace solidity::smtutil;
 
+namespace
+{
+	// HACK to get around Z3 bug in printing type names with spaces (https://github.com/Z3Prover/z3/issues/6850)
+	void sanitizeTypeName(std::string& name)
+	{
+		std::replace(name.begin(), name.end(), ' ', '_');
+		std::replace(name.begin(), name.end(), '(', '[');
+		std::replace(name.begin(), name.end(), ')', ']');
+	}
+}
+
 namespace solidity::frontend::smt
 {
 
@@ -118,13 +130,16 @@ SortPointer smtSort(frontend::Type const& _type)
 			else if (baseType->category() == frontend::Type::Category::FixedBytes)
 				tupleName = "fixedbytes";
 			else
+			{
 				tupleName = arrayType->baseType()->toString(true);
+			}
 
 			tupleName += "_array";
 		}
 		else
 			tupleName = _type.toString(true);
 
+		sanitizeTypeName(tupleName);
 		tupleName += "_tuple";
 
 		return std::make_shared<TupleSort>(
@@ -136,7 +151,9 @@ SortPointer smtSort(frontend::Type const& _type)
 	case Kind::Tuple:
 	{
 		std::vector<std::string> members;
-		auto const& tupleName = _type.toString(true);
+		auto tupleName = _type.toString(true);
+		sanitizeTypeName(tupleName);
+
 		std::vector<SortPointer> sorts;
 
 		if (auto const* tupleType = dynamic_cast<frontend::TupleType const*>(&_type))