diff --git a/mc.cc b/mc.cc
index 315cdc8..e4be58e 100644
--- a/mc.cc
+++ b/mc.cc
@@ -18,6 +18,7 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts)
   pv_succ_E = srs->getEncPVsucc_E();
   pv_ctx_E = srs->getEncPVctx_E();
   pv_proc_enab_E = srs->getEncPVproc_enab_E();
+  pv_drs_E = srs->getEncPVdrs_E();
 
   assert(pv != nullptr);
   assert(pv_succ != nullptr);
@@ -25,6 +26,7 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts)
   assert(pv_succ_E != nullptr);
   assert(pv_ctx_E != nullptr);
   assert(pv_proc_enab_E != nullptr);
+  assert(pv_drs_E != nullptr);
 
   //
   // Transition relations
diff --git a/mc.hh b/mc.hh
index 66307c4..31fe9ae 100644
--- a/mc.hh
+++ b/mc.hh
@@ -26,6 +26,7 @@ class ModelChecker
     BDD *pv_E;
     BDD *pv_succ_E;
     BDD *pv_ctx_E;
+    BDDvec *pv_drs_E;
     BDD *reach;
     vector<BDD> *trp;
     BDD *trm;
diff --git a/rsin_parser.ll b/rsin_parser.ll
index 3bd41f0..20dba91 100644
--- a/rsin_parser.ll
+++ b/rsin_parser.ll
@@ -82,6 +82,14 @@ blank [ \t]
 "U"                     return token::U;
 "F"                     return token::F;
 "G"                     return token::G;
+"UK"                    return token::UK;
+"UC"                    return token::UC;
+"UD"                    return token::UD;
+"UE"                    return token::UE;
+"NK"                    return token::NK;
+"NC"                    return token::NC;
+"ND"                    return token::ND;
+"NE"                    return token::NE;
 "empty"                 return token::EMPTY;
 "#".*                   ;
 
diff --git a/rsin_parser.yy b/rsin_parser.yy
index 6910086..0600a30 100644
--- a/rsin_parser.yy
+++ b/rsin_parser.yy
@@ -49,14 +49,14 @@ class rsin_driver;
 %token CONTEXTAUTOMATON STATES INITSTATE TRANSITIONS
 %token EQ LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL DOT COMMA RARR
 %token AND OR XOR IMPLIES NOT
-%token EX EU EF EG AX AU AF AG E A X U F G EMPTY
+%token EX EU EF EG AX AU AF AG E A X U F G UK UC UD UE NK NC ND NE EMPTY
 
 %token        END      0 "end of file"
 %token <sval> IDENTIFIER "identifier"
 %token <ival> NUMBER     "number"
 
 %left AND OR XOR IMPLIES NOT
-%left EX EU EF EG AX AU AF AG E A X U F G
+%left EX EU EF EG AX AU AF AG E A X U F G UK UC UD UE NK NC ND NE
 
 //%right SRB
 
diff --git a/symrs.cc b/symrs.cc
index 3126496..71f3fbf 100644
--- a/symrs.cc
+++ b/symrs.cc
@@ -166,6 +166,7 @@ void SymRS::initBDDvars(void)
       (*pv_drs)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++);
       (*pv_drs_succ)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++);
 
+      // Quantification (per proc)
       (*pv_drs_E)[proc_id] *= (*pv_drs)[proc_id][i];
 
       // The DRS part of the system (flattened): these vars do not include CA
diff --git a/symrs.hh b/symrs.hh
index 18212b9..5133420 100644
--- a/symrs.hh
+++ b/symrs.hh
@@ -59,6 +59,10 @@ class SymRS
     {
       return pv_proc_enab_E;
     }
+    BDDvec *getEncPVdrs_E(void)
+    {
+      return pv_drs_E;
+    }
     BDDvec *getEncPartTrans(void)
     {
       return partTrans;
@@ -216,7 +220,7 @@ class SymRS
                                        (per DRS process) */
     vector<BDDvec> *pv_drs_succ;  /*!< PVs for the product (successor)
                                        part of state (per DRS process) */
-      
+
     BDDvec *pv_drs_E;             /*!< Quantification BDDs for each process */
 
     BDDvec *pv_drs_flat;          /*!< PVs for the DRS product part of state (flat) */