From 62030bfddd55de9d6813defd2765703697239236 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 10 Feb 2026 22:27:42 +0000 Subject: [PATCH] Simplify svector assignment operators using = default (#8566) Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/util/vector.h | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/util/vector.h b/src/util/vector.h index 74783308e..8d1632ced 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -653,14 +653,8 @@ public: svector(const svector&) = default; svector(svector&&) noexcept = default; - svector & operator=(const svector & source) { - vector::operator=(source); - return *this; - } - svector & operator=(svector && source) noexcept { - vector::operator=(std::move(source)); - return *this; - } + svector & operator=(const svector &) = default; + svector & operator=(svector &&) noexcept = default; };