diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 749353af3ce..e3eaa05834e 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -158,7 +158,9 @@ max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
   return ((mp_integer)1) << (mp_integer)bits_for_positive_offset;
 }
 
-void ansi_c_internal_additions(std::string &code)
+void ansi_c_internal_additions(
+  std::string &code,
+  bool support_ts_18661_3_Floatn_types)
 {
   // clang-format off
   // do the built-in types and variables
@@ -247,9 +249,7 @@ void ansi_c_internal_additions(std::string &code)
     config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
   {
     code+=gcc_builtin_headers_types;
-    // check the parser and not config.ansi_c.ts_18661_3_Floatn_types to adjust
-    // behaviour depending on C or C++ context
-    if(ansi_c_parser.ts_18661_3_Floatn_types)
+    if(support_ts_18661_3_Floatn_types)
       code += gcc_builtin_headers_types_gcc7plus;
 
     // there are many more, e.g., look at
diff --git a/src/ansi-c/ansi_c_internal_additions.h b/src/ansi-c/ansi_c_internal_additions.h
index 735022d6703..c2531b65337 100644
--- a/src/ansi-c/ansi_c_internal_additions.h
+++ b/src/ansi-c/ansi_c_internal_additions.h
@@ -12,7 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <string>
 
-void ansi_c_internal_additions(std::string &code);
+void ansi_c_internal_additions(
+  std::string &code,
+  bool support_ts_18661_3_Floatn_types);
 void ansi_c_architecture_strings(std::string &code);
 
 extern const char clang_builtin_headers[];
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index af29ed2599e..0777f819673 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -68,20 +68,19 @@ bool ansi_c_languaget::parse(
   // parsing
 
   std::string code;
-  ansi_c_internal_additions(code);
+  ansi_c_internal_additions(code, config.ansi_c.ts_18661_3_Floatn_types);
   std::istringstream codestr(code);
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=&codestr;
-  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
 
-  ansi_c_scanner_init();
+  ansi_c_scanner_init(ansi_c_parser);
 
   bool result=ansi_c_parser.parse();
 
@@ -90,7 +89,7 @@ bool ansi_c_languaget::parse(
     ansi_c_parser.set_line_no(0);
     ansi_c_parser.set_file(path);
     ansi_c_parser.in=&i_preprocessed;
-    ansi_c_scanner_init();
+    ansi_c_scanner_init(ansi_c_parser);
     result=ansi_c_parser.parse();
   }
 
@@ -197,13 +196,12 @@ bool ansi_c_languaget::to_expr(
 
   // parsing
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(irep_idt());
   ansi_c_parser.in=&i_preprocessed;
-  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.mode=config.ansi_c.mode;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
-  ansi_c_scanner_init();
+  ansi_c_scanner_init(ansi_c_parser);
 
   bool result=ansi_c_parser.parse();
 
diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp
index 9aa79de4ab4..c26911d93b0 100644
--- a/src/ansi-c/ansi_c_parser.cpp
+++ b/src/ansi-c/ansi_c_parser.cpp
@@ -10,8 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "c_storage_spec.h"
 
-ansi_c_parsert ansi_c_parser;
-
 ansi_c_id_classt ansi_c_parsert::lookup(
   const irep_idt &base_name,
   irep_idt &identifier, // output
@@ -73,14 +71,6 @@ void ansi_c_parsert::add_tag_with_body(irept &tag)
   }
 }
 
-extern char *yyansi_ctext;
-
-int yyansi_cerror(const std::string &error)
-{
-  ansi_c_parser.parse_error(error, yyansi_ctext);
-  return 0;
-}
-
 void ansi_c_parsert::add_declarator(
   exprt &declaration,
   irept &declarator)
diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h
index 4dde7752afe..060a684bf09 100644
--- a/src/ansi-c/ansi_c_parser.h
+++ b/src/ansi-c/ansi_c_parser.h
@@ -18,15 +18,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ansi_c_parse_tree.h"
 #include "ansi_c_scope.h"
 
-int yyansi_cparse();
+class ansi_c_parsert;
+int yyansi_cparse(ansi_c_parsert &);
 
 class ansi_c_parsert:public parsert
 {
 public:
   ansi_c_parse_treet parse_tree;
 
-  ansi_c_parsert()
-    : tag_following(false),
+  explicit ansi_c_parsert(message_handlert &message_handler)
+    : parsert(message_handler),
+      tag_following(false),
       asm_block_following(false),
       parenthesis_counter(0),
       mode(modet::NONE),
@@ -35,11 +37,14 @@ class ansi_c_parsert:public parsert
       for_has_scope(false),
       ts_18661_3_Floatn_types(false)
   {
+    // set up global scope
+    scopes.clear();
+    scopes.push_back(scopet());
   }
 
   virtual bool parse() override
   {
-    return yyansi_cparse()!=0;
+    return yyansi_cparse(*this) != 0;
   }
 
   virtual void clear() override
@@ -166,9 +171,6 @@ class ansi_c_parsert:public parsert
   std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
 };
 
-extern ansi_c_parsert ansi_c_parser;
-
-int yyansi_cerror(const std::string &error);
-void ansi_c_scanner_init();
+void ansi_c_scanner_init(ansi_c_parsert &);
 
 #endif // CPROVER_ANSI_C_ANSI_C_PARSER_H
diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp
index 0d9de3c48cd..80cd8db2905 100644
--- a/src/ansi-c/builtin_factory.cpp
+++ b/src/ansi-c/builtin_factory.cpp
@@ -47,16 +47,15 @@ static bool convert(
 {
   std::istringstream in(s.str());
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=&in;
-  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
 
-  ansi_c_scanner_init();
+  ansi_c_scanner_init(ansi_c_parser);
 
   if(ansi_c_parser.parse())
     return true;
@@ -97,6 +96,7 @@ static bool convert(
 //! \return 'true' on error
 bool builtin_factory(
   const irep_idt &identifier,
+  bool support_ts_18661_3_Floatn_types,
   symbol_table_baset &symbol_table,
   message_handlert &mh)
 {
@@ -106,7 +106,7 @@ bool builtin_factory(
   std::ostringstream s;
 
   std::string code;
-  ansi_c_internal_additions(code);
+  ansi_c_internal_additions(code, support_ts_18661_3_Floatn_types);
   s << code;
 
   // our own extensions
diff --git a/src/ansi-c/builtin_factory.h b/src/ansi-c/builtin_factory.h
index 8a012894c3f..e270d4917f1 100644
--- a/src/ansi-c/builtin_factory.h
+++ b/src/ansi-c/builtin_factory.h
@@ -17,6 +17,7 @@ class symbol_table_baset;
 //! \return 'true' in case of error
 bool builtin_factory(
   const irep_idt &identifier,
+  bool support_ts_18661_3_Floatn_types,
   symbol_table_baset &,
   message_handlert &);
 
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index bbe4948376e..dc0b11a209a 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -250,6 +250,8 @@ class c_typecheck_baset:
 
   virtual bool gcc_types_compatible_p(const typet &, const typet &);
 
+  virtual bool builtin_factory(const irep_idt &);
+
   // types
   virtual void typecheck_type(typet &type);
   virtual void typecheck_compound_type(struct_union_typet &type);
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index df210afc6cf..1879b6a8dc2 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2072,6 +2072,15 @@ void c_typecheck_baset::typecheck_obeys_contract_call(
   expr.type() = bool_typet();
 }
 
+bool c_typecheck_baset::builtin_factory(const irep_idt &identifier)
+{
+  return ::builtin_factory(
+    identifier,
+    config.ansi_c.ts_18661_3_Floatn_types,
+    symbol_table,
+    get_message_handler());
+}
+
 void c_typecheck_baset::typecheck_side_effect_function_call(
   side_effect_expr_function_callt &expr)
 {
@@ -2106,7 +2115,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
         typecheck_typed_target_call(expr);
       }
       // Is this a builtin?
-      else if(!builtin_factory(identifier, symbol_table, get_message_handler()))
+      else if(!builtin_factory(identifier))
       {
         // yes, it's a builtin
       }
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 5335593b46d..f2959d76171 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -13,13 +13,27 @@
 #ifdef ANSI_C_DEBUG
 #define YYDEBUG 1
 #endif
-#define PARSER ansi_c_parser
+#define PARSER (*ansi_c_parser)
 
 #include "ansi_c_parser.h"
 
 int yyansi_clex();
 extern char *yyansi_ctext;
 
+static ansi_c_parsert *ansi_c_parser;
+int yyansi_cparse(void);
+int yyansi_cparse(ansi_c_parsert &_ansi_c_parser)
+{
+  ansi_c_parser = &_ansi_c_parser;
+  return yyansi_cparse();
+}
+
+int yyansi_cerror(const std::string &error)
+{
+  ansi_c_parser->parse_error(error, yyansi_ctext);
+  return 0;
+}
+
 #include "parser_static.inc"
 
 #include "literals/convert_integer_literal.h"
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index a55fc3b1fc0..7794f34bd2e 100644
--- a/src/ansi-c/scanner.l
+++ b/src/ansi-c/scanner.l
@@ -38,7 +38,7 @@ static int isatty(int) { return 0; }
 #include "literals/convert_string_literal.h"
 #include "literals/unescape_string.h"
 
-#define PARSER ansi_c_parser
+#define PARSER (*ansi_c_parser)
 #define YYSTYPE unsigned
 #undef  ECHO
 #define ECHO
@@ -49,6 +49,19 @@ static int isatty(int) { return 0; }
 extern int yyansi_cdebug;
 #endif
 
+static ansi_c_parsert *ansi_c_parser;
+void ansi_c_scanner_init(ansi_c_parsert &_ansi_c_parser)
+{
+#ifdef ANSI_C_DEBUG
+  yyansi_cdebug=1;
+#endif
+  ansi_c_parser = &_ansi_c_parser;
+  YY_FLUSH_BUFFER;
+  BEGIN(0);
+}
+
+int yyansi_cerror(const std::string &error);
+
 #define loc() \
   { newstack(yyansi_clval); PARSER.set_source_location(parser_stack(yyansi_clval)); }
 
@@ -264,17 +277,6 @@ enable_or_disable ("enable"|"disable")
 %x CPROVER_PRAGMA
 %x OTHER_PRAGMA
 
-%{
-void ansi_c_scanner_init()
-{
-#ifdef ANSI_C_DEBUG
-  yyansi_cdebug=1;
-#endif
-  YY_FLUSH_BUFFER;
-  BEGIN(0);
-}
-%}
-
 %%
 
 <INITIAL>.|\n   { BEGIN(GRAMMAR);
diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp
index 7d6ae8351f3..b4bfd5e7dff 100644
--- a/src/cpp/cpp_language.cpp
+++ b/src/cpp/cpp_language.cpp
@@ -102,11 +102,9 @@ bool cpp_languaget::parse(
   std::istringstream i_preprocessed(o_preprocessed.str());
 
   // parsing
-
-  cpp_parser.clear();
+  cpp_parsert cpp_parser{message_handler};
   cpp_parser.set_file(path);
   cpp_parser.in=&i_preprocessed;
-  cpp_parser.log.set_message_handler(message_handler);
   cpp_parser.mode=config.ansi_c.mode;
 
   bool result=cpp_parser.parse();
@@ -245,11 +243,9 @@ bool cpp_languaget::to_expr(
   std::istringstream i_preprocessed(code);
 
   // parsing
-
-  cpp_parser.clear();
+  cpp_parsert cpp_parser{message_handler};
   cpp_parser.set_file(irep_idt());
   cpp_parser.in=&i_preprocessed;
-  cpp_parser.log.set_message_handler(message_handler);
 
   bool result=cpp_parser.parse();
 
diff --git a/src/cpp/cpp_parser.cpp b/src/cpp/cpp_parser.cpp
index 0d72414eec9..c4484638eb8 100644
--- a/src/cpp/cpp_parser.cpp
+++ b/src/cpp/cpp_parser.cpp
@@ -11,25 +11,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_parser.h"
 
-#include <util/config.h>
-
-cpp_parsert cpp_parser;
-
-bool cpp_parse();
+bool cpp_parse(cpp_parsert &, message_handlert &);
 
 bool cpp_parsert::parse()
 {
-  // We use the ANSI-C scanner
-  ansi_c_parser.cpp98=true;
-  ansi_c_parser.cpp11 =
-    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
-    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14 ||
-    config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17;
-  ansi_c_parser.ts_18661_3_Floatn_types=false;
-  ansi_c_parser.in=in;
-  ansi_c_parser.mode=mode;
-  ansi_c_parser.set_file(get_file());
-  ansi_c_parser.log.set_message_handler(log.get_message_handler());
-
-  return cpp_parse();
+  token_buffer.ansi_c_parser.in = in;
+  token_buffer.ansi_c_parser.mode = mode;
+  token_buffer.ansi_c_parser.set_file(get_file());
+  return cpp_parse(*this, log.get_message_handler());
 }
diff --git a/src/cpp/cpp_parser.h b/src/cpp/cpp_parser.h
index 1813872bf76..6029fca6ea2 100644
--- a/src/cpp/cpp_parser.h
+++ b/src/cpp/cpp_parser.h
@@ -34,10 +34,12 @@ class cpp_parsert:public parsert
     asm_block_following=false;
   }
 
-  cpp_parsert():
-    mode(configt::ansi_ct::flavourt::ANSI),
-    recognize_wchar_t(true),
-    asm_block_following(false)
+  explicit cpp_parsert(message_handlert &message_handler)
+    : parsert(message_handler),
+      mode(configt::ansi_ct::flavourt::ANSI),
+      recognize_wchar_t(true),
+      token_buffer(message_handler),
+      asm_block_following(false)
   {
   }
 
@@ -67,6 +69,4 @@ class cpp_parsert:public parsert
   bool asm_block_following;
 };
 
-extern cpp_parsert cpp_parser;
-
 #endif // CPROVER_CPP_CPP_PARSER_H
diff --git a/src/cpp/cpp_token_buffer.cpp b/src/cpp/cpp_token_buffer.cpp
index df7e918f8a7..85a1a56d5bc 100644
--- a/src/cpp/cpp_token_buffer.cpp
+++ b/src/cpp/cpp_token_buffer.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_token_buffer.h"
 
-#include <ansi-c/ansi_c_parser.h>
-
 int cpp_token_buffert::LookAhead(unsigned offset)
 {
   PRECONDITION(current_pos <= token_vector.size());
diff --git a/src/cpp/cpp_token_buffer.h b/src/cpp/cpp_token_buffer.h
index 4d3acdbfc3c..d9b5f20139c 100644
--- a/src/cpp/cpp_token_buffer.h
+++ b/src/cpp/cpp_token_buffer.h
@@ -12,17 +12,28 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_TOKEN_BUFFER_H
 #define CPROVER_CPP_CPP_TOKEN_BUFFER_H
 
+#include <util/config.h>
+#include <util/invariant.h>
+
+#include <ansi-c/ansi_c_parser.h>
+
 #include "cpp_token.h"
 
 #include <list>
 
-#include <util/invariant.h>
-
 class cpp_token_buffert
 {
 public:
-  cpp_token_buffert():current_pos(0)
+  explicit cpp_token_buffert(message_handlert &message_handler)
+    : ansi_c_parser(message_handler), current_pos(0)
   {
+    // We use the ANSI-C scanner
+    ansi_c_parser.cpp98 = true;
+    ansi_c_parser.cpp11 =
+      config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
+      config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14 ||
+      config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17;
+    ansi_c_parser.ts_18661_3_Floatn_types = false;
   }
 
   typedef unsigned int post;
@@ -51,6 +62,8 @@ class cpp_token_buffert
     return tokens.back();
   }
 
+  ansi_c_parsert ansi_c_parser;
+
 protected:
   typedef std::list<cpp_tokent> tokenst;
   tokenst tokens;
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
index 06f6f69009b..6f888c1cb79 100644
--- a/src/cpp/cpp_typecheck.cpp
+++ b/src/cpp/cpp_typecheck.cpp
@@ -325,7 +325,8 @@ void cpp_typecheckt::clean_up()
 
 bool cpp_typecheckt::builtin_factory(const irep_idt &identifier)
 {
-  return ::builtin_factory(identifier, symbol_table, get_message_handler());
+  return ::builtin_factory(
+    identifier, false, symbol_table, get_message_handler());
 }
 
 bool cpp_typecheckt::contains_cpp_name(const exprt &expr)
diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h
index 814b3d8c13e..0e64a2f38cb 100644
--- a/src/cpp/cpp_typecheck.h
+++ b/src/cpp/cpp_typecheck.h
@@ -343,7 +343,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   void add_method_body(symbolt *_method_symbol);
 
-  bool builtin_factory(const irep_idt &);
+  bool builtin_factory(const irep_idt &) override;
 
   // types
 
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index c16a92a6d12..910d91a5811 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -195,10 +195,15 @@ void new_scopet::print_rec(std::ostream &out, unsigned indent) const
 class Parser // NOLINT(readability/identifiers)
 {
 public:
-  explicit Parser(cpp_parsert &_cpp_parser):
-    lex(_cpp_parser.token_buffer),
-    parser(_cpp_parser),
-    max_errors(10)
+  Parser(cpp_parsert &_cpp_parser, message_handlert &message_handler)
+    : lex(_cpp_parser.token_buffer),
+      parse_tree(_cpp_parser.parse_tree),
+      message_handler(message_handler),
+      max_errors(10),
+      cpp11(
+        config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
+        config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14 ||
+        config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17)
   {
     root_scope.kind=new_scopet::kindt::NAMESPACE;
     current_scope=&root_scope;
@@ -208,7 +213,8 @@ class Parser // NOLINT(readability/identifiers)
 
 protected:
   cpp_token_buffert &lex;
-  cpp_parsert &parser;
+  cpp_parse_treet &parse_tree;
+  message_handlert &message_handler;
 
   // scopes
   new_scopet root_scope;
@@ -408,6 +414,7 @@ class Parser // NOLINT(readability/identifiers)
   }
 
   unsigned int max_errors;
+  const bool cpp11;
 };
 
 static bool is_identifier(int token)
@@ -512,8 +519,9 @@ bool Parser::SyntaxError()
 
     message+="'";
 
-    parser.log.error().source_location = source_location;
-    parser.log.error() << message << messaget::eom;
+    messaget log{message_handler};
+    log.error().source_location = source_location;
+    log.error() << message << messaget::eom;
   }
 
   return ++number_of_errors < max_errors;
@@ -1986,13 +1994,10 @@ bool Parser::optStorageSpec(cpp_storage_spect &storage_spec)
 {
   int t=lex.LookAhead(0);
 
-  if(t==TOK_STATIC ||
-     t==TOK_EXTERN ||
-     (t == TOK_AUTO && !ansi_c_parser.cpp11) ||
-     t==TOK_REGISTER ||
-     t==TOK_MUTABLE ||
-     t==TOK_GCC_ASM ||
-     t==TOK_THREAD_LOCAL)
+  if(
+    t == TOK_STATIC || t == TOK_EXTERN || (t == TOK_AUTO && !cpp11) ||
+    t == TOK_REGISTER || t == TOK_MUTABLE || t == TOK_GCC_ASM ||
+    t == TOK_THREAD_LOCAL)
   {
     cpp_tokent tk;
     lex.get_token(tk);
@@ -2730,7 +2735,7 @@ bool Parser::rConstructorDecl(
 
     case TOK_DEFAULT: // C++0x
       {
-        if(!ansi_c_parser.cpp11)
+        if(!cpp11)
         {
           SyntaxError();
           return false;
@@ -2743,7 +2748,7 @@ bool Parser::rConstructorDecl(
 
     case TOK_DELETE: // C++0x
       {
-        if(!ansi_c_parser.cpp11)
+        if(!cpp11)
         {
           SyntaxError();
           return false;
@@ -2907,7 +2912,7 @@ bool Parser::rDeclaratorWithInit(
 
       if(lex.LookAhead(0)==TOK_DEFAULT) // C++0x
       {
-        if(!ansi_c_parser.cpp11)
+        if(!cpp11)
         {
           SyntaxError();
           return false;
@@ -2919,7 +2924,7 @@ bool Parser::rDeclaratorWithInit(
       }
       else if(lex.LookAhead(0)==TOK_DELETE) // C++0x
       {
-        if(!ansi_c_parser.cpp11)
+        if(!cpp11)
         {
           SyntaxError();
           return false;
@@ -8379,7 +8384,7 @@ bool Parser::operator()()
 
   while(rProgram(item))
   {
-    parser.parse_tree.items.push_back(item);
+    parse_tree.items.push_back(item);
     item.clear();
   }
 
@@ -8390,8 +8395,8 @@ bool Parser::operator()()
   return number_of_errors!=0;
 }
 
-bool cpp_parse()
+bool cpp_parse(cpp_parsert &cpp_parser, message_handlert &message_handler)
 {
-  Parser parser(cpp_parser);
+  Parser parser(cpp_parser, message_handler);
   return parser();
 }
diff --git a/src/goto-instrument/contracts/contracts_wrangler.cpp b/src/goto-instrument/contracts/contracts_wrangler.cpp
index b3aab30e54c..7c6dec33105 100644
--- a/src/goto-instrument/contracts/contracts_wrangler.cpp
+++ b/src/goto-instrument/contracts/contracts_wrangler.cpp
@@ -139,11 +139,11 @@ void contracts_wranglert::mangle(
 
   // Parse the fake function.
   std::istringstream is(pr.str());
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser{message_handler};
   ansi_c_parser.set_line_no(0);
   ansi_c_parser.set_file("<predicate>");
   ansi_c_parser.in = &is;
-  ansi_c_scanner_init();
+  ansi_c_scanner_init(ansi_c_parser);
   ansi_c_parser.parse();
 
   // Extract the invariants from prase_tree.
diff --git a/src/util/parser.h b/src/util/parser.h
index 70a796ec4a9..c19aeb58977 100644
--- a/src/util/parser.h
+++ b/src/util/parser.h
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_PARSER_H
 #define CPROVER_UTIL_PARSER_H
 
+#include "deprecate.h"
 #include "expr.h"
 #include "message.h"
 
@@ -39,7 +40,13 @@ class parsert
     last_line.clear();
   }
 
+  DEPRECATED(SINCE(2023, 12, 20, "use parsert(message_handler) instead"))
   parsert():in(nullptr) { clear(); }
+  explicit parsert(message_handlert &message_handler)
+    : in(nullptr), log(message_handler)
+  {
+    clear();
+  }
   virtual ~parsert() { }
 
   // The following are for the benefit of the scanner