From b27a2aa7fc66c88efa8d6535b91e4d23eefd1fe9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 16 Feb 2025 10:13:00 -0800
Subject: [PATCH] remove calls to removed def constructor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_arith_base.cpp       | 2 --
 src/ast/sls/sls_seq_plugin.cpp       | 6 +++---
 src/muz/spacer/spacer_qe_project.cpp | 5 ++---
 src/qe/qe.cpp                        | 2 +-
 src/qe/qe_mbp.cpp                    | 2 +-
 src/sat/smt/q_mbi.cpp                | 4 ++--
 src/smt/theory_seq.cpp               | 2 +-
 7 files changed, 10 insertions(+), 13 deletions(-)

diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 479134eae..b8a3c2abe 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -536,9 +536,7 @@ namespace sls {
 
     template<typename num_t>
     void arith_base<num_t>::add_update_idiv(op_def const& od, num_t const& delta) {
-        num_t arg1 = value(od.m_arg1);
         num_t arg2 = value(od.m_arg2);
-
         if (arg2 != 0) {
             if (arg2 > 0)
                 add_update(od.m_arg1, delta * arg2);
diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
index 1e14a6932..f74261da2 100644
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@@ -414,7 +414,7 @@ namespace sls {
                 return ev.val1.svalue;
             }
             case OP_SEQ_EXTRACT: {
-                expr* x, * offset, * len;
+                expr* x = nullptr, * offset = nullptr, * len = nullptr;
                 VERIFY(seq.str.is_extract(e, x, offset, len));
                 zstring r = strval0(x);
                 expr_ref offset_e = ctx.get_value(offset);
@@ -449,7 +449,7 @@ namespace sls {
                 }
             }
             case OP_SEQ_REPLACE: {
-                expr* x, * y, * z;
+                expr* x = nullptr, * y = nullptr, * z = nullptr;
                 VERIFY(seq.str.is_replace(e, x, y, z));
                 zstring r = strval0(x);
                 zstring s = strval0(y);
@@ -458,7 +458,7 @@ namespace sls {
                 return ev.val1.svalue;
             }
             case OP_SEQ_REPLACE_ALL: {
-                expr* x, * y, * z;
+                expr* x = nullptr, * y = nullptr, * z = nullptr;
                 VERIFY(seq.str.is_replace_all(e, x, y, z));
                 zstring s1 = strval0(x);
                 zstring s2 = strval0(y);
diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp
index eef728c02..b2dabf161 100644
--- a/src/muz/spacer/spacer_qe_project.cpp
+++ b/src/muz/spacer/spacer_qe_project.cpp
@@ -1937,7 +1937,6 @@ class array_project_selects_util {
                 todo.pop_back();
                 continue;
             }
-            unsigned num_args = a->get_num_args();
             bool all_done = true;
             for (auto arg : *a) {
                 if (!done.is_marked(arg) && is_app(arg)) {
@@ -1945,13 +1944,13 @@ class array_project_selects_util {
                     all_done = false;
                 }
             }
-            if (!all_done) continue;
+            if (!all_done)
+                continue;
             todo.pop_back();
             if (m_arr_u.is_select(a)) {
                 expr *arr = a->get_arg(0);
                 if (m_arr_test.is_marked(arr)) {
                     ptr_vector<app> *lst = m_sel_terms.find(to_app(arr));
-                    ;
                     lst->push_back(a);
                 }
             }
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index cfd863711..189953dcd 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -2472,7 +2472,7 @@ namespace qe {
             for_each_expr(p, fml);
             return false;
         }
-        catch (found) {
+        catch (found const&) {
             return true;
         }
     }
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index e8ce2777b..147bd9b5f 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({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..881515f37 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({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({v, t});                        
                     }
                 }
                 add_instantiation(q, body);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 25a73ae56..182398e9c 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1542,7 +1542,7 @@ void theory_seq::add_length(expr* l) {
 void theory_seq::init_length_limit_for_contains(expr* c) {
     if (ctx.is_searching())
         return;
-    expr* x, *y;
+    expr* x = nullptr, *y = nullptr;
     VERIFY(m_util.str.is_contains(c, x, y));
     unsigned min_y = m_util.str.min_length(y);
     if (min_y > 0) {