From cf5a8fd248e5ae3a5f83246939d8ad0680b166f5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 21 Jul 2022 08:58:32 -0700
Subject: [PATCH] fix validation code for pb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/smt/pb_solver.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index dc2bb71dd..13d3e02e4 100644
--- a/src/sat/smt/pb_solver.cpp
+++ b/src/sat/smt/pb_solver.cpp
@@ -1823,7 +1823,7 @@ namespace pb {
}
bool solver::validate_watch(pbc const& p, literal alit) const {
- if (value(p.lit()) != l_true)
+ if (p.lit() == sat::null_literal || value(p.lit()) != l_true)
return true;
for (unsigned i = 0; i < p.size(); ++i) {
literal l = p[i].second;