diff --git a/regression/statement-list/Add_Int/test.desc b/regression/statement-list/Add_Int/test.desc
index a4385da4279..afa12c06879 100644
--- a/regression/statement-list/Add_Int/test.desc
+++ b/regression/statement-list/Add_Int/test.desc
@@ -3,7 +3,7 @@ main.awl
 --show-parse-tree
 ^EXIT=0$
 ^SIGNAL=0$
-^Name: "Add_Int"$
+^Name: Add_Int$
 ^Version: 0[.]1$
 ^  \* type: signedbv$
 ^      \* width: 16$
diff --git a/regression/statement-list/Add_Int2/main.awl b/regression/statement-list/Add_Int2/main.awl
index 80a6f4704fe..d3f928bf234 100644
--- a/regression/statement-list/Add_Int2/main.awl
+++ b/regression/statement-list/Add_Int2/main.awl
@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Add_Int2"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_INPUT 
       in1 : Int;
diff --git a/regression/statement-list/Add_Int2/test.desc b/regression/statement-list/Add_Int2/test.desc
index bbf4830a91d..13d2530c816 100644
--- a/regression/statement-list/Add_Int2/test.desc
+++ b/regression/statement-list/Add_Int2/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Add_Int2\"
+
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/statement-list/Arithmetic/main.awl b/regression/statement-list/Arithmetic/main.awl
index 2aa832d14bc..bffa90c0d2e 100644
--- a/regression/statement-list/Arithmetic/main.awl
+++ b/regression/statement-list/Arithmetic/main.awl
@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Arithmetic"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_TEMP 
       compResult : Bool;
diff --git a/regression/statement-list/Arithmetic/test.desc b/regression/statement-list/Arithmetic/test.desc
index 60576b9bbf3..13d2530c816 100644
--- a/regression/statement-list/Arithmetic/test.desc
+++ b/regression/statement-list/Arithmetic/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Arithmetic\"
+
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/statement-list/Bool1/test.desc b/regression/statement-list/Bool1/test.desc
index 6caf68dd16d..e0528e08d37 100644
--- a/regression/statement-list/Bool1/test.desc
+++ b/regression/statement-list/Bool1/test.desc
@@ -3,7 +3,7 @@ main.awl
 --show-parse-tree
 ^EXIT=0$
 ^SIGNAL=0$
-^Name: "Bool1"$
+^Name: Bool1$
 ^Version: 0[.]1$
 ^  \* type: bool$
 ^  \* identifier: in1$
diff --git a/regression/statement-list/Bool2/main.awl b/regression/statement-list/Bool2/main.awl
index 1e2c013ac3d..63c354259b3 100644
--- a/regression/statement-list/Bool2/main.awl
+++ b/regression/statement-list/Bool2/main.awl
@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Bool2"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_INPUT 
       in1 : Bool;
diff --git a/regression/statement-list/Bool2/test.desc b/regression/statement-list/Bool2/test.desc
index 5e21dd6bb97..48435b6da54 100644
--- a/regression/statement-list/Bool2/test.desc
+++ b/regression/statement-list/Bool2/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Bool2\"
+
 ^EXIT=10$
 ^SIGNAL=0$
 ^SAT checker: instance is SATISFIABLE$
diff --git a/regression/statement-list/Bool3/main.awl b/regression/statement-list/Bool3/main.awl
index 1d0120cbe68..dc1a0f47c3c 100644
--- a/regression/statement-list/Bool3/main.awl
+++ b/regression/statement-list/Bool3/main.awl
@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Bool3"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_INPUT 
       in1 : Bool;
diff --git a/regression/statement-list/Bool3/test.desc b/regression/statement-list/Bool3/test.desc
index b6c9799ef8d..f6ef8634b0d 100644
--- a/regression/statement-list/Bool3/test.desc
+++ b/regression/statement-list/Bool3/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Bool3\"
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^\*\* 0 of 1 failed \(1 iterations\)$
diff --git a/regression/statement-list/Bool4/main.awl b/regression/statement-list/Bool4/main.awl
index 8e31722833a..6b37525d857 100644
--- a/regression/statement-list/Bool4/main.awl
+++ b/regression/statement-list/Bool4/main.awl
@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Bool4"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_TEMP 
       temp1 : Bool;
diff --git a/regression/statement-list/Bool4/test.desc b/regression/statement-list/Bool4/test.desc
index 3de6d88bfbf..b67aeca7c14 100644
--- a/regression/statement-list/Bool4/test.desc
+++ b/regression/statement-list/Bool4/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Bool4\"
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/statement-list/Bool5/main.awl b/regression/statement-list/Bool5/main.awl
index 5dbf7784a1d..346b4f45315 100644
--- a/regression/statement-list/Bool5/main.awl
+++ b/regression/statement-list/Bool5/main.awl
@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Bool5"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_INPUT 
       in1 : Bool;
diff --git a/regression/statement-list/Bool5/test.desc b/regression/statement-list/Bool5/test.desc
index 5ac35659259..f6ef8634b0d 100644
--- a/regression/statement-list/Bool5/test.desc
+++ b/regression/statement-list/Bool5/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Bool5\"
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^\*\* 0 of 1 failed \(1 iterations\)$
diff --git a/regression/statement-list/Div_Real/test.desc b/regression/statement-list/Div_Real/test.desc
index eea28dcc9f1..fb04e55fe71 100644
--- a/regression/statement-list/Div_Real/test.desc
+++ b/regression/statement-list/Div_Real/test.desc
@@ -3,7 +3,7 @@ main.awl
 --show-parse-tree
 ^EXIT=0$
 ^SIGNAL=0$
-^Name: "Div_Real"$
+^Name: Div_Real$
 ^Version: 0[.]1$
 ^  \* type: floatbv$
 ^      \* width: 32$
diff --git a/regression/statement-list/Function_Call1/test.desc b/regression/statement-list/Function_Call1/test.desc
index 05b229262ad..3fe4a9c1139 100644
--- a/regression/statement-list/Function_Call1/test.desc
+++ b/regression/statement-list/Function_Call1/test.desc
@@ -3,9 +3,9 @@ main.awl
 --show-parse-tree
 ^EXIT=0$
 ^SIGNAL=0$
-^Name: "Function_Call1"$
+^Name: Function_Call1$
 ^Version: 0[.]1$
-^statement_list_call	"__Function"$
+^statement_list_call	__Function$
 ^	param := In1$
 --
 ^warning: ignoring
diff --git a/regression/statement-list/Function_Call2/test.desc b/regression/statement-list/Function_Call2/test.desc
index 9afe8d2a1a6..d57c7589ea1 100644
--- a/regression/statement-list/Function_Call2/test.desc
+++ b/regression/statement-list/Function_Call2/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Function_Call2\"
+--function Function_Call2
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/statement-list/Mul_DInt/test.desc b/regression/statement-list/Mul_DInt/test.desc
index 76649cd0934..2b6b2dce0a4 100644
--- a/regression/statement-list/Mul_DInt/test.desc
+++ b/regression/statement-list/Mul_DInt/test.desc
@@ -3,7 +3,7 @@ main.awl
 --show-parse-tree
 ^EXIT=0$
 ^SIGNAL=0$
-^Name: "Mul_DInt"$
+^Name: Mul_DInt$
 ^Version: 0[.]1$
 ^  \* type: signedbv$
 ^      \* width: 32$
diff --git a/regression/statement-list/Multiple_Elements/test.desc b/regression/statement-list/Multiple_Elements/test.desc
index de72c04c521..3aa343eea39 100644
--- a/regression/statement-list/Multiple_Elements/test.desc
+++ b/regression/statement-list/Multiple_Elements/test.desc
@@ -3,8 +3,8 @@ main.awl
 --show-parse-tree
 ^EXIT=0$
 ^SIGNAL=0$
-^Name: "Mult_1"$
-^Name: "Mult_2"$
-^Name: "Mult_3"$
+^Name: Mult_1$
+^Name: Mult_2$
+^Name: Mult_3$
 --
 ^warning: ignoring
diff --git a/regression/statement-list/Sub_DInt/main.awl b/regression/statement-list/Sub_DInt/main.awl
index cc93f926e44..dfcc720fed5 100644
--- a/regression/statement-list/Sub_DInt/main.awl
+++ b/regression/statement-list/Sub_DInt/main.awl
@@ -1,4 +1,4 @@
-FUNCTION_BLOCK "Sub_DInt"
+FUNCTION_BLOCK "Main"
 VERSION : 0.1
    VAR_INPUT 
       in1 : DInt;
diff --git a/regression/statement-list/Sub_DInt/test.desc b/regression/statement-list/Sub_DInt/test.desc
index 13fae121572..48435b6da54 100644
--- a/regression/statement-list/Sub_DInt/test.desc
+++ b/regression/statement-list/Sub_DInt/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.awl
---function \"Sub_DInt\"
+
 ^EXIT=10$
 ^SIGNAL=0$
 ^SAT checker: instance is SATISFIABLE$
diff --git a/regression/statement-list/Var_Declaration/test.desc b/regression/statement-list/Var_Declaration/test.desc
index 937379af610..942893abe4a 100644
--- a/regression/statement-list/Var_Declaration/test.desc
+++ b/regression/statement-list/Var_Declaration/test.desc
@@ -3,8 +3,8 @@ main.awl
 --show-parse-tree
 ^EXIT=0$
 ^SIGNAL=0$
-^Name: "Var_assign_FB"$
-^Name: "Var_assign_FC"$
+^Name: Var_assign_FB$
+^Name: Var_assign_FC$
 ^Version: 0[.]1$
 ^  \* type: bool$
 ^  \* type: floatbv$
diff --git a/src/statement-list/scanner.l b/src/statement-list/scanner.l
index 892942eff35..6ede333edcb 100644
--- a/src/statement-list/scanner.l
+++ b/src/statement-list/scanner.l
@@ -21,6 +21,8 @@
 #include <util/pragma_wnull_conversion.def>
 #include <util/pragma_wdeprecated_register.def>
 
+#include <algorithm>
+
 // Visual Studio
 #if defined _MSC_VER
 // Disable warning for signed/unsigned mismatch.
@@ -75,6 +77,7 @@ void statement_list_scanner_init()
 
 %x GRAMMAR
 %x TAG_NAME
+%x MODULE_NAME
 %x TAG_ATTRIBUTES
 %x VERSION_ANNOTATION
 
@@ -90,9 +93,9 @@ void statement_list_scanner_init()
   TAG                 { loc(); BEGIN(TAG_NAME); return TOK_TAG; }
   BEGIN               { loc(); return TOK_BEGIN; }
   VERSION             { loc(); BEGIN(VERSION_ANNOTATION); return TOK_VERSION; }
-  FUNCTION_BLOCK      { loc(); return TOK_FUNCTION_BLOCK; }
+  FUNCTION_BLOCK      { loc(); BEGIN(MODULE_NAME); return TOK_FUNCTION_BLOCK; }
   END_FUNCTION_BLOCK  { loc(); return TOK_END_FUNCTION_BLOCK; }
-  FUNCTION            { loc(); return TOK_FUNCTION; }
+  FUNCTION            { loc(); BEGIN(MODULE_NAME); return TOK_FUNCTION; }
   END_FUNCTION        { loc(); return TOK_END_FUNCTION; }
   VAR_INPUT           { loc(); return TOK_VAR_INPUT; }
   VAR_OUTPUT          { loc(); return TOK_VAR_OUTPUT; }
@@ -110,7 +113,7 @@ void statement_list_scanner_init()
   Void                { loc(); return TOK_VOID; }
   L                   { loc(); return TOK_LOAD; }
   T                   { loc(); return TOK_TRANSFER; }
-  CALL                { loc(); return TOK_CALL; }
+  CALL                { loc(); BEGIN(MODULE_NAME); return TOK_CALL; }
   NOP                 { loc(); return TOK_NOP; }
   SET                 { loc(); return TOK_SET_RLO; }
   CLR                 { loc(); return TOK_CLR_RLO; }
@@ -292,6 +295,24 @@ void statement_list_scanner_init()
                       }
   END_TAG             { loc(); BEGIN(GRAMMAR); return TOK_END_TAG; }
 }
+
+<MODULE_NAME>{
+  [\t\r\n ]           ;
+  \"[^\"\r\t\n]+\"    {
+                        newstack(yystatement_listlval);
+                        std::string str{yytext};
+                        str.erase(
+                          std::remove(begin(str), end(str), '\"' ), 
+                          end(str));
+                        parser_stack(yystatement_listlval) = 
+                          convert_identifier(str);
+                        PARSER.set_source_location(
+                          parser_stack(yystatement_listlval));
+                        BEGIN(GRAMMAR);
+                        return TOK_IDENTIFIER; 
+                      }
+}
+
 <TAG_ATTRIBUTES>{
   [\t\r," ]           ;
   ([t|T][R|r][u|U][e|E])|([f|F][a|A][l|L][s|S][e|E]) ;
diff --git a/src/statement-list/statement_list_typecheck.cpp b/src/statement-list/statement_list_typecheck.cpp
index 13380f934e7..afde15561b4 100644
--- a/src/statement-list/statement_list_typecheck.cpp
+++ b/src/statement-list/statement_list_typecheck.cpp
@@ -30,9 +30,9 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 /// Postfix for the type of a data block.
 #define DATA_BLOCK_TYPE_POSTFIX "_db"
 /// Name of the CBMC assert function.
-#define CPROVER_ASSERT "\"" CPROVER_PREFIX "assert\""
+#define CPROVER_ASSERT CPROVER_PREFIX "assert"
 /// Name of the CBMC assume function.
-#define CPROVER_ASSUME "\"" CPROVER_PREFIX "assume\""
+#define CPROVER_ASSUME CPROVER_PREFIX "assume"
 /// Name of the RLO symbol used in some operations.
 #define CPROVER_TEMP_RLO CPROVER_PREFIX "temp_rlo"
 
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 4b5b4b92a79..ef2676574d3 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -766,7 +766,7 @@ IREP_ID_TWO(statement_list, Statement List)
 IREP_ID_ONE(statement_list_type)
 IREP_ID_ONE(statement_list_function)
 IREP_ID_ONE(statement_list_function_block)
-IREP_ID_TWO(statement_list_main_function, "Main")
+IREP_ID_TWO(statement_list_main_function, Main)
 IREP_ID_ONE(statement_list_data_block)
 IREP_ID_ONE(statement_list_version)
 IREP_ID_ONE(statement_list_var_input)