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))) {