diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index e05bed9a7..fbff2e583 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -435,12 +435,11 @@ namespace qe { }; class div_rewriter_cfg : public default_rewriter_cfg { - nlqsat& s; ast_manager& m; arith_util a; vector
m_divs; public: - div_rewriter_cfg(nlqsat& s): s(s), m(s.m), a(s.m) {} + div_rewriter_cfg(nlqsat& s): m(s.m), a(s.m) {} ~div_rewriter_cfg() {} br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) { if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && !a.is_numeral(args[1]) && is_ground(args[0]) && is_ground(args[1])) { diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index e50821256..73f6a9d4c 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -503,13 +503,11 @@ namespace qe { } class kernel { - ast_manager& m; smt_params m_smtp; smt::kernel m_kernel; public: kernel(ast_manager& m): - m(m), m_kernel(m, m_smtp) { m_smtp.m_model = true;