From bf3c213fd3edd1ac063e4e6caafa8962e2cd4e9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 Jan 2022 11:03:29 -0800 Subject: [PATCH] #5753 --- src/sat/smt/q_solver.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index b1169e175..d58b9b4d0 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -228,12 +228,13 @@ namespace q { } bool solver::expand(quantifier* q) { - expr_ref r(m); + expr_ref r(q, m); proof_ref pr(m); - m_der(q, r, pr); + ctx.rewrite(r); + m_der(r, r, pr); m_expanded.reset(); if (r != q) { - ctx.get_rewriter()(r); + ctx.rewrite(r); m_expanded.push_back(r); return true; }