From 5206e29bddccdad63bd61a50d6e3678aa9215a3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Feb 2018 09:18:05 -0800 Subject: [PATCH] fix wrong check Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index e5dd057bb..259b1550a 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -2672,11 +2672,11 @@ namespace sat { return; } - VERIFY(c.size() - c.k() >= sz - k); + VERIFY(!all_units || c.size() - c.k() >= sz - k); c.set_size(sz); c.set_k(k); - if (clausify(c)) { + if (all_units && clausify(c)) { return; }