From 71cbb160d2be95f9d33ce3de6286de4e258afad1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Dec 2021 14:29:43 -0800 Subject: [PATCH] fix regression from today, see #5676 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_theory.cpp | 7 ------- src/smt/theory_user_propagator.cpp | 12 +++++++++++- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index fb8d61e8a..0c876e8bc 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -150,13 +150,6 @@ namespace smt { literal theory::mk_literal(expr* _e) { expr_ref e(_e, m); - if (has_quantifiers(e)) { - expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m); - expr_ref eq(m.mk_eq(fn, e), m); - ctx.assert_expr(eq); - ctx.internalize_assertions(); - return mk_literal(fn); - } bool is_not = m.is_not(_e, _e); if (!ctx.e_internalized(_e)) { ctx.internalize(_e, is_quantifier(_e)); diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 722e3343d..e70e75c8c 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -146,7 +146,17 @@ void theory_user_propagator::propagate() { lit.neg(); for (auto const& [a,b] : m_eqs) m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false)); - literal lit = mk_literal(prop.m_conseq); + + literal lit; + if (has_quantifiers(prop.m_conseq)) { + expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m); + expr_ref eq(m.mk_eq(fn, prop.m_conseq), m); + ctx.assert_expr(eq); + ctx.internalize_assertions(); + lit = mk_literal(fn); + } + else + lit = mk_literal(prop.m_conseq); ctx.mark_as_relevant(lit); m_lits.push_back(lit); ctx.mk_th_lemma(get_id(), m_lits);