diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index 71c86efe0..bafbd247d 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -52,8 +52,7 @@ namespace sls {
         m_plugins.set(p->fid(), p);
     }
 
-    void context::ensure_plugin(expr* e) {
-        auto fid = get_fid(e);
+    void context::ensure_plugin(family_id fid) {
         if (m_plugins.get(fid, nullptr))
             return;
         else if (fid == arith_family_id)
@@ -67,9 +66,14 @@ namespace sls {
         else if (fid == array_util(m).get_family_id())
             register_plugin(alloc(array_plugin, *this));
         else
-            verbose_stream() << "did not find plugin for " << mk_bounded_pp(e, m) << "\n";
-            
-        // add arrays and bv dynamically too.
+            verbose_stream() << "did not find plugin for " << fid << "\n";
+    }
+
+    void context::ensure_plugin(expr* e) {
+        auto fid = get_fid(e);
+        ensure_plugin(fid);
+        fid = e->get_sort()->get_family_id();
+        ensure_plugin(fid);           
     }
 
 
diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index 4eccba0bc..f0e1cedca 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -136,6 +136,7 @@ namespace sls {
         void repair_literals();
 
         void ensure_plugin(expr* e);
+        void ensure_plugin(family_id fid);
         family_id get_fid(expr* e) const;
 
 
diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index aee13acc8..b55e9fadd 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -24,6 +24,7 @@ Todo:
 #include "ast/sls/sls_euf_plugin.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
+#include "params/sls_params.hpp"
 
 
 namespace sls {
@@ -37,7 +38,8 @@ namespace sls {
     euf_plugin::~euf_plugin() {}
 
     void euf_plugin::initialize() {
-        m_incremental = ctx.get_params().get_bool("euf_incremental", m_incremental);
+        sls_params sp(ctx.get_params());
+        m_incremental = sp.euf_incremental();
         IF_VERBOSE(2, verbose_stream() << "sls.euf: incremental " << m_incremental << "\n");
     }