From f63c9e366fad52638dc5c413fa6262c238468d26 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Apr 2025 17:29:09 -0700 Subject: [PATCH] disable assignment for param_descrs --- src/util/params.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/params.h b/src/util/params.h index 200b4aa2c..c499dd56e 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -115,6 +115,7 @@ class param_descrs { public: param_descrs(); ~param_descrs(); + param_descrs& operator=(param_descrs const&) = delete; void copy(param_descrs & other); void insert(char const * name, param_kind k, char const * descr, char const * def = nullptr, char const* module = nullptr); void insert(symbol const & name, param_kind k, char const * descr, char const * def = nullptr, char const* module = nullptr);