mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

ignore propagation on units

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-11 15:10:44 -08:00
parent 6a72a4fc00
commit 4d0bc8c8b3
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_win_dist.py
View file

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

2
src/sat/sat_solver.cpp
View file

@ -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