From d7ffd67e6810f362c6a39605a2eaad20e943dfd6 Mon Sep 17 00:00:00 2001
From: Jevin Sweval <jevinsweval@gmail.com>
Date: Sun, 16 Feb 2025 13:06:36 -0500
Subject: [PATCH] Build fix for eee96ec: create mbp::def w/ brace
 initialization

eee96ec removed the explicit constructor for mbp_plugin.h's struct def.
Change qe_mbp.cpp and q_mbi.cpp to use brace initialization.
---
 src/qe/qe_mbp.cpp     | 2 +-
 src/sat/smt/q_mbi.cpp | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

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);