diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 355e9a3d5..00353e4b4 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1211,7 +1211,8 @@ namespace smt {
    
         while (m_num_marks > 0) {
 
-            //m_lemma.normalize();
+            m_lemma.normalize();
+            TRACE("pb", display(tout, m_lemma, true););
             SASSERT(m_lemma.well_formed());         
 
             //