From 22ff73e85a6033ef111f057fbf72107bf00db2f0 Mon Sep 17 00:00:00 2001
From: Pawel Gebal <pawel.gebal@imapp.pl>
Date: Fri, 12 Apr 2024 18:29:16 +0200
Subject: [PATCH] Fix internal error when using an empty tuple with a ternary
 operator

---
 Changelog.md                                   |  1 +
 libsmtutil/Z3Interface.cpp                     |  6 ++++++
 .../ternary_operator_with_functions.sol        | 11 +++++++++++
 .../operators/ternary_operator_with_tuple.sol  | 18 ++++++++++++++++++
 4 files changed, 36 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/operators/ternary_operator_with_functions.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/ternary_operator_with_tuple.sol

diff --git a/Changelog.md b/Changelog.md
index ccc2de41a6ce..d07200ed2613 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -8,6 +8,7 @@ Compiler Features:
 
 Bugfixes:
  * SMTChecker: Fix internal error on mapping access caused by too strong requirements on sort compatibility of the index and mapping domain.
+ * SMTChecker: Fix internal error when using an empty tuple in a conditional operator.
  * SMTChecker: Fix internal error when using bitwise operators with an array element as argument.
 
 
diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp
index 1cfbc815f78e..4e1d1cec1236 100644
--- a/libsmtutil/Z3Interface.cpp
+++ b/libsmtutil/Z3Interface.cpp
@@ -169,6 +169,12 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 				smtAssert(sortSort, "");
 				return m_context.constant(n.c_str(), z3Sort(*sortSort->inner));
 			}
+			else if (n == "tuple_constructor")
+			{
+				auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, z3Sort(*_expr.sort)));
+				smtAssert(constructor.arity() == arguments.size());
+				return constructor();
+			}
 			else
 				try
 				{
diff --git a/test/libsolidity/smtCheckerTests/operators/ternary_operator_with_functions.sol b/test/libsolidity/smtCheckerTests/operators/ternary_operator_with_functions.sol
new file mode 100644
index 000000000000..8214862e7c82
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/ternary_operator_with_functions.sol
@@ -0,0 +1,11 @@
+contract C {
+	function f() public {}
+	function g() public {}
+
+	function test() public {
+		true ? f() : g();
+	}
+}
+// ====
+// SMTEngine: all
+// ----
diff --git a/test/libsolidity/smtCheckerTests/operators/ternary_operator_with_tuple.sol b/test/libsolidity/smtCheckerTests/operators/ternary_operator_with_tuple.sol
new file mode 100644
index 000000000000..d05d699c3373
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/ternary_operator_with_tuple.sol
@@ -0,0 +1,18 @@
+contract C {
+	function empty_tuple() public pure {
+		true ? () : (); // bug fix test, proper handling of empty tuples
+	}
+
+	function non_empty_tuple() public pure {
+		true ? (1, 2) : (3, 4);
+	}
+
+	function return_empty_tuple() public pure {
+		return true ? () : ();
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6133: (53-67): Statement has no effect.
+// Warning 6133: (166-188): Statement has no effect.