diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index e8ce2777b..5553a62da 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -487,7 +487,7 @@ public:
                 val = model(var);
                 sub.insert(var, val);
                 if (defs)
-                    defs->push_back(mbp::def(expr_ref(var, m), val));
+                    defs->push_back(mbp::def{expr_ref(var, m), val});
                 unsigned j = 0;
                 for (expr* f : fmls) {
                     sub(f, tmp);
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index 07d4880c9..4e175b550 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -367,7 +367,7 @@ namespace q {
             TRACE("euf", tout << "replaced model value " << term << "\nfrom\n" << val << "\n");
             rep.insert(v, term);
             if (ctx.use_drat())
-                m_defs.push_back(mbp::def(expr_ref(v, m), term));
+                m_defs.push_back(mbp::def{expr_ref(v, m), term});
             eqs.push_back(m.mk_eq(v, val));
         }
         rep(fmls);
@@ -569,7 +569,7 @@ namespace q {
                     for (unsigned i = 0; i < binding.size(); ++i) {
                         expr_ref v(qb.vars.get(i), m);
                         expr_ref t(binding.get(i), m);
-                        m_defs.push_back(mbp::def(v, t));
+                        m_defs.push_back(mbp::def{v, t});
                     }
                 }
                 add_instantiation(q, body);