From dd0b0b47b827cffd506c602099574676d1f5d2a5 Mon Sep 17 00:00:00 2001 From: Hari Govind V K Date: Fri, 4 Aug 2023 15:18:16 -0700 Subject: [PATCH] fix #5925 (#6846) --- src/qe/mbp/mbp_term_graph.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp index 7af5e88a4..83a1f3c58 100644 --- a/src/qe/mbp/mbp_term_graph.cpp +++ b/src/qe/mbp/mbp_term_graph.cpp @@ -770,7 +770,7 @@ void term_graph::mk_qe_lite_equalities(term &t, expr_ref_vector &out, it = &it->get_next()) { tout << *it << "\n"; };); DEBUG_CODE( for (term *it = &t.get_next(); it != &t; it = &it->get_next()) - SASSERT(!it->is_cgr() || + SASSERT(!it->is_cgr() || it->is_eq_or_neq() || contains_nc(mk_app_core(it->get_expr())));); return; }