diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 1f11b9bf5..1885fc9c4 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -772,6 +772,7 @@ namespace smt {
     void theory_pb::assign_eh(bool_var v, bool is_true) {
         ptr_vector<ineq>* ineqs = 0;
         literal nlit(v, is_true);
+        init_watch(v);
         TRACE("pb", tout << "assign: " << ~nlit << "\n";);
         ineqs = m_var_infos[v].m_lit_watch[nlit.sign()];
         if (ineqs != 0) {
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index 7f621f9c5..ee68bd26e 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -216,9 +216,6 @@ namespace smt {
         theory_pb_params         m_params;        
 
         svector<var_info>        m_var_infos; 
-//        u_map<watch_list*>       m_lwatch;      // per literal.
-//        u_map<watch_list*>       m_vwatch;      // per variable.
-//        u_map<ineq*>             m_ineqs;       // per inequality.
         arg_map                  m_ineq_rep;       // Simplex: representative inequality
         u_map<row_info>          m_ineq_row_info;  // Simplex: row information per variable
         uint_set                 m_vars;           // Simplex: 0-1 variables.