From 02acc38c28d20aff249e27bae2504539444bf225 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Sep 2021 08:53:47 -0700 Subject: [PATCH] add extra checks that user-supplied assumptions are asserted Signed-off-by: Nikolaj Bjorner --- src/smt/user_propagator.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp index 5769a34e5da..ca99e9768a7 100644 --- a/src/smt/user_propagator.cpp +++ b/src/smt/user_propagator.cpp @@ -125,6 +125,8 @@ void user_propagator::propagate() { for (auto const& p : prop.m_eqs) m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second))); DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root());); + DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id));); + DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true);); if (m.is_false(prop.m_conseq)) { js = ctx.mk_justification(