diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
index 4608a99960a..2ac73696f7e 100644
--- a/src/solvers/smt2/smt2_parser.cpp
+++ b/src/solvers/smt2/smt2_parser.cpp
@@ -818,10 +818,7 @@ exprt smt2_parsert::function_application()
           if(id_it->second.type.id()==ID_mathematical_function)
           {
             return function_application_exprt(
-              symbol_exprt(final_id, id_it->second.type),
-              op,
-              to_mathematical_function_type(
-                id_it->second.type).codomain());
+              symbol_exprt(final_id, id_it->second.type), op);
           }
           else
             return symbol_exprt(final_id, id_it->second.type);
diff --git a/src/util/mathematical_expr.cpp b/src/util/mathematical_expr.cpp
index 28118cf6317..062226e3816 100644
--- a/src/util/mathematical_expr.cpp
+++ b/src/util/mathematical_expr.cpp
@@ -7,3 +7,17 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include "mathematical_expr.h"
+#include "mathematical_types.h"
+
+function_application_exprt::function_application_exprt(
+  const symbol_exprt &_function,
+  argumentst _arguments)
+  : binary_exprt(
+      _function,
+      ID_function_application,
+      multi_ary_exprt(irep_idt(), std::move(_arguments), typet()),
+      to_mathematical_function_type(_function.type()).codomain())
+{
+  const auto &domain = to_mathematical_function_type(_function.type()).domain();
+  PRECONDITION(domain.size() == arguments().size());
+}
diff --git a/src/util/mathematical_expr.h b/src/util/mathematical_expr.h
index 226aba5552a..de8bcde3427 100644
--- a/src/util/mathematical_expr.h
+++ b/src/util/mathematical_expr.h
@@ -192,6 +192,7 @@ class function_application_exprt : public binary_exprt
 public:
   using argumentst = exprt::operandst;
 
+  DEPRECATED("use function_application_exprt(fkt, arg) instead")
   function_application_exprt(
     const symbol_exprt &_function,
     const argumentst &_arguments,
@@ -201,6 +202,10 @@ class function_application_exprt : public binary_exprt
     arguments() = _arguments;
   }
 
+  function_application_exprt(
+    const symbol_exprt &_function,
+    argumentst _arguments);
+
   symbol_exprt &function()
   {
     return static_cast<symbol_exprt &>(op0());