diff --git a/src/util/params.cpp b/src/util/params.cpp
index 4911664f1..aefe4e074 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -565,6 +565,8 @@ void params_ref::set(params_ref const & p) {
 void params_ref::copy(params_ref const & src) {
     if (m_params == nullptr || m_params->empty())
         set(src);
+    else if (src.empty())
+        return;
     else {
         init();
         copy_core(src.m_params);