From 51d62684e1c94349496513232346e3af114147f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Mar 2018 15:51:00 -0700 Subject: [PATCH] move propagation to after binary clause addition Signed-off-by: Nikolaj Bjorner --- src/sat/sat_asymm_branch.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 3e306370d..ae6db1f6c 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -416,6 +416,7 @@ namespace sat { case 2: SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); s.mk_bin_clause(c[0], c[1], c.is_learned()); + if (s.m_trail.size() > s.m_qhead) s.propagate_core(false); scoped_d.del_clause(); return false; default: @@ -459,9 +460,7 @@ namespace sat { // try asymmetric branching // clause must not be used for propagation - s.propagate(false); - if (s.inconsistent()) - return true; + scoped_detach scoped_d(s, c); unsigned new_sz = c.size(); unsigned flip_position = m_rand(c.size());