diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
index d52bb8eafa1..d71454d4fd0 100644
--- a/src/solvers/smt2/smt2_parser.cpp
+++ b/src/solvers/smt2/smt2_parser.cpp
@@ -1028,26 +1028,27 @@ typet smt2_parsert::function_signature_definition()
     return sort();
   }
 
-  mathematical_function_typet result;
+  mathematical_function_typet::domaint domain;
 
   while(peek()!=CLOSE)
   {
     if(next_token()!=OPEN)
     {
       error() << "expected '(' at beginning of parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
     if(next_token()!=SYMBOL)
     {
       error() << "expected symbol in parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
-    auto &var=result.add_variable();
+    mathematical_function_typet::variablet var;
     std::string id=buffer;
     var.set_identifier(id);
     var.type()=sort();
+    domain.push_back(var);
 
     auto &entry=id_map[id];
     entry.type=var.type();
@@ -1056,15 +1057,15 @@ typet smt2_parsert::function_signature_definition()
     if(next_token()!=CLOSE)
     {
       error() << "expected ')' at end of parameter" << eom;
-      return result;
+      return nil_typet();
     }
   }
 
   next_token(); // eat the ')'
 
-  result.codomain()=sort();
+  typet codomain = sort();
 
-  return result;
+  return mathematical_function_typet(domain, codomain);
 }
 
 typet smt2_parsert::function_signature_declaration()
@@ -1081,37 +1082,38 @@ typet smt2_parsert::function_signature_declaration()
     return sort();
   }
 
-  mathematical_function_typet result;
+  mathematical_function_typet::domaint domain;
 
   while(peek()!=CLOSE)
   {
     if(next_token()!=OPEN)
     {
       error() << "expected '(' at beginning of parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
     if(next_token()!=SYMBOL)
     {
       error() << "expected symbol in parameter" << eom;
-      return result;
+      return nil_typet();
     }
 
-    auto &var=result.add_variable();
+    mathematical_function_typet::variablet var;
     var.type()=sort();
+    domain.push_back(var);
 
     if(next_token()!=CLOSE)
     {
       error() << "expected ')' at end of parameter" << eom;
-      return result;
+      return nil_typet();
     }
   }
 
   next_token(); // eat the ')'
 
-  result.codomain()=sort();
+  typet codomain = sort();
 
-  return result;
+  return mathematical_function_typet(domain, codomain);
 }
 
 void smt2_parsert::command(const std::string &c)
diff --git a/src/util/std_types.h b/src/util/std_types.h
index 701cbf159a0..ca2c0934685 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -1686,11 +1686,6 @@ inline complex_typet &to_complex_type(typet &type)
 class mathematical_function_typet:public typet
 {
 public:
-  mathematical_function_typet():typet(ID_mathematical_function)
-  {
-    subtypes().resize(2);
-  }
-
   // the domain of the function is composed of zero, one, or
   // many variables
   class variablet:public irept
@@ -1720,6 +1715,14 @@ class mathematical_function_typet:public typet
 
   using domaint=std::vector<variablet>;
 
+  mathematical_function_typet(const domaint &_domain, const typet &_codomain)
+    : typet(ID_mathematical_function)
+  {
+    subtypes().resize(2);
+    domain() = _domain;
+    codomain() = _codomain;
+  }
+
   domaint &domain()
   {
     return (domaint &)subtypes()[0].subtypes();