ignore propagation on units

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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):

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