From f0b0ce401e5089e377de2257f323b739c7ef5fd3 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 7 Feb 2024 15:16:44 +0100
Subject: [PATCH] take std::function as const reference

---
 src/ast/euf/euf_bv_plugin.cpp | 6 +++---
 src/ast/euf/euf_bv_plugin.h   | 8 ++++----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp
index 6930a9807..4a078e9ef 100644
--- a/src/ast/euf/euf_bv_plugin.cpp
+++ b/src/ast/euf/euf_bv_plugin.cpp
@@ -426,7 +426,7 @@ namespace euf {
         push_merge(n0, n);        
     }
 
-    void bv_plugin::sub_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer) {
+    void bv_plugin::sub_slices(enode* n, std::function<bool(enode*, unsigned)> const& consumer) {
         m_todo.push_back({ n, 0 });
         unsigned lo, hi;
         expr* e;
@@ -461,7 +461,7 @@ namespace euf {
         clear_offsets();
     }
 
-    void bv_plugin::super_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer) {
+    void bv_plugin::super_slices(enode* n, std::function<bool(enode*, unsigned)> const& consumer) {
         m_todo.push_back({ n, 0 });
         unsigned lo, hi;
         expr* e;
@@ -500,7 +500,7 @@ namespace euf {
     // Explain that a is a subslice of b at offset
     // or that b is a subslice of a at offset
     // 
-    void bv_plugin::explain_slice(enode* a, unsigned offset, enode* b, std::function<void(enode*, enode*)>& consumer) {
+    void bv_plugin::explain_slice(enode* a, unsigned offset, enode* b, std::function<void(enode*, enode*)> const& consumer) {
         if (width(a) < width(b))
             std::swap(a, b);
         SASSERT(width(a) >= width(b));
diff --git a/src/ast/euf/euf_bv_plugin.h b/src/ast/euf/euf_bv_plugin.h
index ec2c0b448..d47445054 100644
--- a/src/ast/euf/euf_bv_plugin.h
+++ b/src/ast/euf/euf_bv_plugin.h
@@ -109,15 +109,15 @@ namespace euf {
 
         void undo() override;
 
-        void set_ensure_th_var(std::function<void(enode*)>& f) { m_ensure_th_var = f; }
+        void set_ensure_th_var(std::function<void(enode*)> f) { m_ensure_th_var = std::move(f); }
         
         std::ostream& display(std::ostream& out) const override;
 
-        void sub_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer);
+        void sub_slices(enode* n, std::function<bool(enode*, unsigned)> const& consumer);
 
-        void super_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer);
+        void super_slices(enode* n, std::function<bool(enode*, unsigned)> const& consumer);
 
-        void explain_slice(enode* a, unsigned offset, enode* b, std::function<void(enode*, enode*)>& consumer);
+        void explain_slice(enode* a, unsigned offset, enode* b, std::function<void(enode*, enode*)> const& consumer);
             
     };
 }