From e33f7281282b3798c57bfc0e9bcdea00cc74aee9 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 31 Oct 2022 15:54:56 +0100 Subject: [PATCH] hm --- src/math/polysat/variable_elimination.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/math/polysat/variable_elimination.cpp b/src/math/polysat/variable_elimination.cpp index 7cdbad5d1..6f0579b25 100644 --- a/src/math/polysat/variable_elimination.cpp +++ b/src/math/polysat/variable_elimination.cpp @@ -95,6 +95,12 @@ namespace polysat { LOG("c_target: " << lit_pp(s, c_target)); LOG("c_new: " << lit_pp(s, c_new)); + // New constraint is already true (maybe we already derived it previously?) + // TODO: It might make sense to keep different derivations of the same constraint. + // E.g., if the new clause could derive c_new at a lower decision level. + if (c_new.bvalue(s) == l_true) + continue; + clause_builder cb(s); for (auto [w, wv] : a) cb.push(~s.eq(s.var(w), wv));