From 290b4dfabcd47c5be600ea2c28742b5ff6d4e55d Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Wed, 19 Feb 2020 17:23:17 +0100 Subject: [PATCH] More cases needed to find all ite clauses. --- src/sat/sat_aig_finder.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_aig_finder.cpp b/src/sat/sat_aig_finder.cpp index 8195674f7..eba4366ae 100644 --- a/src/sat/sat_aig_finder.cpp +++ b/src/sat/sat_aig_finder.cpp @@ -217,8 +217,11 @@ namespace sat { if (c.size() != 3 || c.was_used()) continue; literal x = c[0], y = c[1], z = c[2]; if (try_ite(x, z, y, c)) continue; + if (try_ite(x, y, z, c)) continue; if (try_ite(y, x, z, c)) continue; - if (try_ite(z, y, x, c)) continue; + if (try_ite(z, x, y, c)) continue; + if (try_ite(z, y, x, c)) continue; + if (try_ite(y, z, x, c)) continue; } std::function not_used = [](clause* cp) { return !cp->was_used(); };