From ead414c4ee8e72c1d9fad7bcdae7aa4a357cf51c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 4 Dec 2013 13:11:58 -0800
Subject: [PATCH] add back skipped consequences, exposed by fu-malik assertion
 violation

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

diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index d8d90b19a..e5686e2e2 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1251,6 +1251,7 @@ namespace smt {
                 justification* cjs = cls.get_justification();
                 if (cjs) {
                     IF_VERBOSE(0, verbose_stream() << "skipping justification for clause over: " << conseq << "\n";);
+                    m_ineq_literals.push_back(conseq);
                     break;
                 }
                 unsigned num_lits = cls.get_num_literals();
@@ -1282,6 +1283,7 @@ namespace smt {
                 // only process pb justifications.
                 if (j.get_from_theory() != get_id()) {
                     IF_VERBOSE(0, verbose_stream() << "skipping justification for " << conseq << "\n";);
+                    m_ineq_literals.push_back(conseq);
                     break;
                 }
                 pb_justification& pbj = dynamic_cast<pb_justification&>(j);