From 8cb959127f79a860bcfbe3da10ce76a0d1ae3dba Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 17 Nov 2013 10:41:15 -0800
Subject: [PATCH] pb theory

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

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;