From fbf834f4c4dc1bc00b2c97d08eb4bb844827520a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 9 Dec 2013 15:48:58 -0800
Subject: [PATCH] debugging pb

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_pb.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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());         
 
             //