diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 4af6f1f0f..d6fe7e5db 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -444,6 +444,7 @@ namespace smt {
         if (c.lit().sign() == is_true) {
             c.negate();
         }
+        SASSERT(c.well_formed());
 
         context& ctx = get_context();
         numeral maxsum = 0;