Fix internal error when using an empty tuple with a ternary operator

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.
 
 

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
 				{

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
+// ----

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.