From 3379155a63de1544f36ec9a492c45069de3ed33a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Jan 2025 03:14:14 -0800 Subject: [PATCH] add check for root literal assignment --- src/ast/sls/sls_context.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index f0acdf426..0ef4d8a04 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -142,6 +142,10 @@ namespace sls { if (m_new_constraint || !unsat().empty()) return l_undef; + // check if root literals got flipped. is-sat assumes root literals are true + if (any_of(root_literals(), [&](sat::literal lit) { return !is_true(lit); })) + continue; + if (all_of(m_plugins, [&](auto* p) { return !p || p->is_sat(); })) { VERIFY(unsat().empty() || !m_new_constraint); values2model();