diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index 577dc46ee..4260d4690 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -86,6 +86,7 @@ namespace sls {
         virtual void force_restart() = 0;
         virtual std::ostream& display(std::ostream& out) = 0;
         virtual reslimit& rlimit() = 0;
+        virtual unsigned timestamp(sat::bool_var v) = 0;
     };
     
     class context {
@@ -195,6 +196,7 @@ namespace sls {
         void shift_weights() { s.shift_weights(); }
         bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) { return s.try_rotate(v, rotated, budget); }
         double reward(sat::bool_var v) { return s.reward(v); }
+        unsigned timestamp(sat::bool_var v) { return s.timestamp(v); }
         indexed_uint_set const& unsat() const { return s.unsat(); }
         indexed_uint_set const& unsat_vars() const { return s.unsat_vars(); }
         unsigned num_external_in_unsat_vars() const { return s.num_external_in_unsat_vars(); }
diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h
index e0b4cbcfe..d3a1077ea 100644
--- a/src/ast/sls/sls_smt_plugin.h
+++ b/src/ast/sls/sls_smt_plugin.h
@@ -186,5 +186,6 @@ namespace sls {
             m_new_clause_added = true;
         }
         void force_restart() override { m_ddfw->force_restart(); }
+        unsigned timestamp(sat::bool_var v) override { return m_ddfw->timestamp(v); }
     };
 }
diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp
index 58aeb5eb7..d92970a04 100644
--- a/src/ast/sls/sls_smt_solver.cpp
+++ b/src/ast/sls/sls_smt_solver.cpp
@@ -102,6 +102,7 @@ namespace sls {
         void add_input_assertion(expr* f) { m_context.add_input_assertion(f); }
         reslimit& rlimit() override { return m_ddfw.rlimit(); }
         void shift_weights() override { m_ddfw.shift_weights(); }
+        unsigned timestamp(sat::bool_var v) override { return m_ddfw.timestamp(v); }
 
         void force_restart() override { m_ddfw.force_restart(); }
 
diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp
index ba27ab2bd..8123edf30 100644
--- a/src/test/sls_test.cpp
+++ b/src/test/sls_test.cpp
@@ -37,6 +37,7 @@ namespace bv {
         void force_restart() override {}
         std::ostream& display(std::ostream& out)  override { return out; }
         reslimit& rlimit() override { return m_limit; }
+        unsigned timestamp(sat::bool_var v) override { return 0; }
     };
 
     class sls_test {