diff --git a/src/ast/sls/sat_ddfw.h b/src/ast/sls/sat_ddfw.h
index 24af8b207..7338be515 100644
--- a/src/ast/sls/sat_ddfw.h
+++ b/src/ast/sls/sat_ddfw.h
@@ -270,11 +270,12 @@ namespace sat {
 
         inline unsigned num_vars() const { return m_vars.size(); }
 
-        std::initializer_list<unsigned> use_list(literal lit) { 
+
+        ptr_iterator<unsigned> use_list(literal lit) { 
             unsigned i = lit.index();
             auto const* b = m_flat_use_list.data() + m_use_list_index[i];
             auto const* e = m_flat_use_list.data() + m_use_list_index[i + 1];
-            return std::initializer_list(b, e);
+            return { b, e };            
         }
 
     };
diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index ba0054d79..d24d7697f 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -52,13 +52,13 @@ namespace sls {
         virtual void set_value(expr* e, expr* v) = 0;
     };
 
-    using clause = std::initializer_list <sat::literal>;
+    using clause = ptr_iterator<sat::literal>;
 
     class sat_solver_context {
     public:
         virtual vector<sat::clause_info> const& clauses() const = 0;
         virtual sat::clause_info const& get_clause(unsigned idx) const = 0;
-        virtual std::initializer_list<unsigned> get_use_list(sat::literal lit) = 0;
+        virtual ptr_iterator<unsigned> get_use_list(sat::literal lit) = 0;
         virtual void flip(sat::bool_var v) = 0;
         virtual double reward(sat::bool_var v) = 0;
         virtual double get_weigth(unsigned clause_idx) = 0;
@@ -126,7 +126,7 @@ namespace sls {
         // expose sat_solver to plugins
         vector<sat::clause_info> const& clauses() const { return s.clauses(); }
         sat::clause_info const& get_clause(unsigned idx) const { return s.get_clause(idx); }
-        std::initializer_list<unsigned> get_use_list(sat::literal lit) { return s.get_use_list(lit); }
+        ptr_iterator<unsigned> get_use_list(sat::literal lit) { return s.get_use_list(lit); }
         double get_weight(unsigned clause_idx) { return s.get_weigth(clause_idx); }
         unsigned num_bool_vars() const { return s.num_vars(); }
         bool is_true(sat::literal lit) { return s.is_true(lit); }  
diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp
index 2f287a680..0de1fbe42 100644
--- a/src/ast/sls/sls_smt_solver.cpp
+++ b/src/ast/sls/sls_smt_solver.cpp
@@ -74,7 +74,7 @@ namespace sls {
 
         vector<sat::clause_info> const& clauses() const override { return m_ddfw.clauses(); }
         sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw.get_clause_info(idx); }
-        std::initializer_list<unsigned> get_use_list(sat::literal lit) override { return m_ddfw.use_list(lit); }
+        ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return m_ddfw.use_list(lit); }
         void flip(sat::bool_var v) override { m_ddfw.flip(v); }
         double reward(sat::bool_var v) override { return m_ddfw.get_reward(v); }
         double get_weigth(unsigned clause_idx) override { return m_ddfw.get_clause_info(clause_idx).m_weight; }
diff --git a/src/sat/smt/sls_solver.cpp b/src/sat/smt/sls_solver.cpp
index 3c3d4566c..3f244e233 100644
--- a/src/sat/smt/sls_solver.cpp
+++ b/src/sat/smt/sls_solver.cpp
@@ -125,7 +125,7 @@ namespace sls {
 
         vector<sat::clause_info> const& clauses() const override { return m_ddfw->clauses(); }
         sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw->get_clause_info(idx); }
-        std::initializer_list<unsigned> get_use_list(sat::literal lit) override { return m_ddfw->use_list(lit); }
+        ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return m_ddfw->use_list(lit); }
         void flip(sat::bool_var v) override { m_ddfw->flip(v); }
         double reward(sat::bool_var v) override { return m_ddfw->get_reward(v); }
         double get_weigth(unsigned clause_idx) override { return m_ddfw->get_clause_info(clause_idx).m_weight; }
diff --git a/src/util/util.h b/src/util/util.h
index cf0146b12..7d1265b33 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -326,6 +326,16 @@ void force_ptr_array_size(T & v, unsigned sz) {
     }
 }
 
+template<typename T>
+class ptr_iterator {
+    T const* b;
+    T const* e;
+public:
+    ptr_iterator(T const* b, T const* e): b(b), e(e) {}
+    T const* begin() const { return b; }
+    T const* end() const { return e; }
+};
+
 class random_gen {
     unsigned m_data;
 public: