From 5566965a5aa99a1880b46ffeaa640fe0da14c66e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 8 Dec 2013 18:19:10 -0800
Subject: [PATCH] fix bug exposed from relevancy

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

diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index e5686e2e2..e43db8dce 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -528,6 +528,9 @@ namespace smt {
         if (ctx.get_assignment(c.lit()) == l_undef) {
             return;
         }
+        if (!ctx.is_relevant(c.lit())) {
+            return;
+        }
         numeral sum = numeral::zero(), maxsum = numeral::zero();
         for (unsigned i = 0; i < c.size(); ++i) {
             switch(ctx.get_assignment(c.lit(i))) {