From 4d0bc8c8b35e16d9510f0e886458311d7e627083 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Nov 2018 15:10:44 -0800 Subject: [PATCH] ignore propagation on units Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.py | 2 +- src/sat/sat_solver.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 10bb5a6ef..9e0374192 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -267,7 +267,7 @@ def cp_vs_runtime(x64): # we use a "check_root" filter to find some hopefully suitable # redistributable. def check_root(root): - return platform in root and "CRT" in root and "onecore" not in root and "debug" not in root + return platform in root and ("CRT" in root or "MP" in root) and "onecore" not in root and "debug" not in root for root, dirs, files in os.walk(path): for filename in files: if fnmatch(filename, '*.dll') and check_root(root): diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index f38da472f..1881d0375 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -920,7 +920,7 @@ namespace sat { if (c[0] == not_l) std::swap(c[0], c[1]); CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";); - if (c.was_removed() || c[1] != not_l) { + if (c.was_removed() || c.size() == 1 || c[1] != not_l) { // Remark: this method may be invoked when the watch lists are not in a consistent state, // and may contain dead/removed clauses, or clauses with removed literals. // See: method propagate_unit at sat_simplifier.cpp