From 019acdb1ef153c0e5e19deae72a5ddb4560ae93c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Mar 2020 19:56:18 -0700 Subject: [PATCH] fix #3350 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_utvpi_def.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index e4a36581d..54d544b6f 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -508,7 +508,7 @@ namespace smt { while (consistent && can_propagate()) { unsigned idx = m_asserted_atoms[m_asserted_qhead]; m_asserted_qhead++; - consistent = propagate_atom(m_atoms[idx]); + consistent = propagate_atom(m_atoms[idx]); } } @@ -520,7 +520,7 @@ namespace smt { return false; } int edge_id = a.get_asserted_edge(); - if (!enable_edge(edge_id)) { + if (!enable_edge(edge_id) || !is_consistent()) { m_graph.traverse_neg_cycle2(m_params.m_arith_stronger_lemmas, m_nc_functor); set_conflict(); return false;