diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h
index de1a1cb56..94b1238c0 100644
--- a/src/ast/sls/bv_sls_eval.h
+++ b/src/ast/sls/bv_sls_eval.h
@@ -138,7 +138,7 @@ namespace bv {
     public:
         sls_eval(sls_terms& terms, sls::context& ctx);
 
-        void tighten_range() { m_fix.init(); }
+        void init() { m_fix.init(); }
 
         void register_term(expr* e);
 
diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 7285bd89b..b7a800292 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -486,7 +486,6 @@ namespace sls {
     typename arith_base<num_t>::var_t arith_base<num_t>::mk_op(arith_op_kind k, expr* e, expr* x, expr* y) {
         auto v = mk_var(e);
         auto w = mk_term(x);
-	//        auto u = mk_term(y);
         unsigned idx = m_ops.size();
         num_t val;
         switch (k) {
diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp
index 8e5fd94a8..ad0f3f99d 100644
--- a/src/ast/sls/sls_bv_plugin.cpp
+++ b/src/ast/sls/sls_bv_plugin.cpp
@@ -61,7 +61,7 @@ namespace sls {
 
     void bv_plugin::initialize() {
         if (!m_initialized) {
-            m_eval.tighten_range();
+            m_eval.init();
             m_initialized = true;
         }
     }
diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp
index 07888a7e9..64961abc2 100644
--- a/src/test/sls_test.cpp
+++ b/src/test/sls_test.cpp
@@ -55,6 +55,9 @@ namespace bv {
             sls::context ctx(m, solver);
             sls_terms terms(ctx);
             sls_eval ev(terms, ctx);
+            for (auto e : es)
+                ev.register_term(e);
+            ev.init();
             th_rewriter rw(m);
             expr_ref r(e, m);
             rw(r);
@@ -171,6 +174,9 @@ namespace bv {
             sls::context ctx(m, solver);
             sls_terms terms(ctx);
             sls_eval ev(terms, ctx);
+            for (auto e : es)
+                ev.register_term(e);
+            ev.init();
 
             if (m.is_bool(e1)) {
                 SASSERT(m.is_true(r) || m.is_false(r));