diff --git a/src/statement-list/parser.y b/src/statement-list/parser.y
index 70b2ccce969..fa21cba3a09 100644
--- a/src/statement-list/parser.y
+++ b/src/statement-list/parser.y
@@ -23,8 +23,17 @@
 
 #include <iterator>
 
-int yystatement_listlex();
-extern char *yystatement_listtext;
+int yystatement_listlex(void *);
+char *yystatement_listget_text(void *);
+
+int yystatement_listerror(
+  statement_list_parsert &statement_list_parser,
+  void *scanner,
+  const std::string &error)
+{
+  statement_list_parser.parse_error(error, yystatement_listget_text(scanner));
+  return 0;
+}
 
 #define YYSTYPE unsigned
 #define YYSTYPE_IS_TRIVIAL 1
@@ -43,9 +52,13 @@ extern char *yystatement_listtext;
 // Disable warning for unreachable code.
 #pragma warning(disable:4702)
 #endif
+%}
+
+%parse-param {statement_list_parsert &statement_list_parser}
+%parse-param {void *scanner}
+%lex-param {void *scanner}
 
 /*** Token declaration *******************************************************/
-%}
 
 /*** STL file structure keywords *********************************************/
 %token TOK_VERSION              "VERSION"
diff --git a/src/statement-list/scanner.l b/src/statement-list/scanner.l
index a06e11cf1f6..b6f080771d9 100644
--- a/src/statement-list/scanner.l
+++ b/src/statement-list/scanner.l
@@ -41,7 +41,7 @@ static int isatty(int) { return 0; }
 #endif
 
 // Value inside of statement_list_parser.h.
-#define PARSER statement_list_parser
+#define PARSER (*yyextra)
 
 // Sets the type of yystatement_listlval so that it can be used as the stack 
 // index.
@@ -58,22 +58,12 @@ static int isatty(int) { return 0; }
 #define loc() \
   { newstack(yystatement_listlval); \
     PARSER.set_source_location(parser_stack(yystatement_listlval)); }
-  
-#ifdef STATEMENT_LIST_DEBUG
-extern int yystatement_listdebug;
-#endif
-void statement_list_scanner_init()
-{
-#ifdef STATEMENT_LIST_DEBUG
-  yystatement_listdebug=1;
-#endif
-  YY_FLUSH_BUFFER;
-  BEGIN(0);
-}
 %}
 %option noyywrap
 %option noinput
 %option nounput
+%option reentrant
+%option extra-type="statement_list_parsert *"
 
 %x GRAMMAR
 %x TAG_NAME
diff --git a/src/statement-list/statement_list_language.cpp b/src/statement-list/statement_list_language.cpp
index bd5e28d185c..d1cc36b7b5b 100644
--- a/src/statement-list/statement_list_language.cpp
+++ b/src/statement-list/statement_list_language.cpp
@@ -60,12 +60,11 @@ bool statement_list_languaget::parse(
   const std::string &path,
   message_handlert &message_handler)
 {
-  statement_list_parser.clear();
+  statement_list_parsert statement_list_parser{message_handler};
   parse_path = path;
   statement_list_parser.set_line_no(0);
   statement_list_parser.set_file(path);
   statement_list_parser.in = &instream;
-  statement_list_scanner_init();
   bool result = statement_list_parser.parse();
 
   // store result
diff --git a/src/statement-list/statement_list_parser.cpp b/src/statement-list/statement_list_parser.cpp
index a5f10b1ff1e..53f43340146 100644
--- a/src/statement-list/statement_list_parser.cpp
+++ b/src/statement-list/statement_list_parser.cpp
@@ -21,9 +21,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 #include <iostream>
 #include <iterator>
 
-statement_list_parsert statement_list_parser;
-
-extern char *yystatement_listtext;
+int statement_list_parsert::instance_count = 0;
 
 /// Searches for the name of the TIA module inside of its root
 /// expression.
@@ -335,15 +333,23 @@ void statement_list_parsert::add_function(const exprt &function)
   parse_tree.add_function(fn);
 }
 
-bool statement_list_parsert::parse()
-{
-  return yystatement_listparse() != 0;
-}
+int yystatement_listlex_init_extra(statement_list_parsert *, void **);
+int yystatement_listlex_destroy(void *);
+/// Defined in statement_list_y.tab.cpp. Main function for the parse process
+/// generated by bison, performs all necessary steps to fill the parse tree.
+int yystatement_listparse(statement_list_parsert &, void *);
+void yystatement_listset_debug(int, void *);
 
-int yystatement_listerror(const std::string &error)
+bool statement_list_parsert::parse()
 {
-  statement_list_parser.parse_error(error, yystatement_listtext);
-  return 0;
+  void *scanner;
+  yystatement_listlex_init_extra(this, &scanner);
+#ifdef STATEMENT_LIST_DEBUG
+  yystatement_listset_debug(1, scanner);
+#endif
+  bool parse_fail = yystatement_listparse(*this, scanner) != 0;
+  yystatement_listlex_destroy(scanner);
+  return parse_fail;
 }
 
 void statement_list_parsert::clear()
diff --git a/src/statement-list/statement_list_parser.h b/src/statement-list/statement_list_parser.h
index 468e35ce05b..79b5f4f7919 100644
--- a/src/statement-list/statement_list_parser.h
+++ b/src/statement-list/statement_list_parser.h
@@ -16,10 +16,6 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 
 #include "statement_list_parse_tree.h"
 
-/// Defined in statement_list_y.tab.cpp. Main function for the parse process
-/// generated by bison, performs all necessary steps to fill the parse tree.
-int yystatement_listparse();
-
 /// Responsible for starting the parse process and to translate the result into
 /// a statement_list_parse_treet. This parser works by using the expression
 /// stack of its base class. During the parse process, expressions with
@@ -34,6 +30,22 @@ int yystatement_listparse();
 class statement_list_parsert : public parsert
 {
 public:
+  /// Constructor
+  explicit statement_list_parsert(message_handlert &message_handler)
+    : parsert(message_handler)
+  {
+    // Simplistic check that we don't attempt to do reentrant parsing as the
+    // Bison-generated parser has global state.
+    PRECONDITION(++instance_count == 1);
+  }
+
+  statement_list_parsert(const statement_list_parsert &) = delete;
+
+  ~statement_list_parsert() override
+  {
+    --instance_count;
+  }
+
   /// Starts the parsing process and saves the result inside of this instance's
   /// parse tree.
   /// \return False if successful.
@@ -69,19 +81,19 @@ class statement_list_parsert : public parsert
 private:
   /// Tree that is being filled by the parsing process.
   statement_list_parse_treet parse_tree;
-};
 
-/// Instance of the parser, used by other modules.
-extern statement_list_parsert statement_list_parser;
+  static int instance_count;
+};
 
 /// Forwards any errors that are encountered during the parse process. This
 /// function gets called by the generated files of flex and bison.
+/// \param parser: Parser object.
+/// \param scanner: Lexer state.
 /// \param error: Error message.
 /// \return Always 0.
-int yystatement_listerror(const std::string &error);
-
-/// Defined in scanner.l. This function initialises the scanner by setting
-/// debug flags (if present) and its initial state.
-void statement_list_scanner_init();
+int yystatement_listerror(
+  statement_list_parsert &parser,
+  void *scanner,
+  const std::string &error);
 
 #endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_PARSER_H