From 8bec1e25a83e8e3f8c9b48f1641b68b6df841f08 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Mar 2017 08:32:06 +0100 Subject: [PATCH] move restore relevancy until after literals have been replayed Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 3fca7d04b..9336322f7 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3747,7 +3747,6 @@ namespace smt { // of the new conflict clause. if (relevancy()) record_relevancy(num_lits, lits); unsigned num_bool_vars = pop_scope_core(m_scope_lvl - new_lvl); - if (relevancy()) restore_relevancy(num_lits, lits); SASSERT(m_scope_lvl == new_lvl); // the logical context may still be in conflict after // clauses are reinitialized in pop_scope. @@ -3778,6 +3777,7 @@ namespace smt { } } } + if (relevancy()) restore_relevancy(num_lits, lits); // Resetting the cache manually because I did not invoke pop_scope, but pop_scope_core reset_cache_generation(); TRACE("resolve_conflict_bug",