diff --git a/regression/smt2_solver/function-applications/function-application3.desc b/regression/smt2_solver/function-applications/function-application3.desc
new file mode 100644
index 00000000000..9ef06444bb1
--- /dev/null
+++ b/regression/smt2_solver/function-applications/function-application3.desc
@@ -0,0 +1,7 @@
+CORE
+function-application3.smt2
+
+^EXIT=20$
+^SIGNAL=0$
+^\(error "line 4: wrong number of arguments for function"\)$
+--
diff --git a/regression/smt2_solver/function-applications/function-application3.smt2 b/regression/smt2_solver/function-applications/function-application3.smt2
new file mode 100644
index 00000000000..9860364c282
--- /dev/null
+++ b/regression/smt2_solver/function-applications/function-application3.smt2
@@ -0,0 +1,6 @@
+(set-logic LIA)
+
+(define-fun next ((x Int)) Int x )
+(assert (= (next ) 243))
+
+(check-sat)
diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
index 674c3afcd98..3db2057bd4f 100644
--- a/src/solvers/smt2/smt2_parser.cpp
+++ b/src/solvers/smt2/smt2_parser.cpp
@@ -291,26 +291,22 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
 }
 
 exprt smt2_parsert::function_application(
-  const irep_idt &,
-  const exprt::operandst &)
+  const symbol_exprt &function,
+  const exprt::operandst &op)
 {
-  #if 0
-  const auto &f = id_map[identifier];
+  const auto &function_type = to_mathematical_function_type(function.type());
 
   // check the arguments
-  if(op.size()!=f.type.variables().size())
+  if(op.size() != function_type.domain().size())
     throw error("wrong number of arguments for function");
 
   for(std::size_t i=0; i<op.size(); i++)
   {
-    if(op[i].type() != f.type.variables()[i].type())
+    if(op[i].type() != function_type.domain()[i])
       throw error("wrong type for arguments for function");
   }
 
-  return function_application_exprt(
-    symbol_exprt(identifier, f.type), op, f.type.range());
-  #endif
-  return nil_exprt();
+  return function_application_exprt(function, op);
 }
 
 exprt::operandst smt2_parsert::cast_bv_to_signed(const exprt::operandst &op)
@@ -826,7 +822,7 @@ exprt smt2_parsert::function_application()
         {
           if(id_it->second.type.id()==ID_mathematical_function)
           {
-            return function_application_exprt(
+            return function_application(
               symbol_exprt(final_id, id_it->second.type), op);
           }
           else
diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h
index 56cd1fa065f..540fcabc376 100644
--- a/src/solvers/smt2/smt2_parser.h
+++ b/src/solvers/smt2/smt2_parser.h
@@ -136,7 +136,7 @@ class smt2_parsert
   exprt let_expression();
   exprt quantifier_expression(irep_idt);
   exprt function_application(
-    const irep_idt &identifier,
+    const symbol_exprt &function,
     const exprt::operandst &op);
 
   /// Apply typecast to signedbv to expressions in vector