diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h
index 81a0796b8..c82161647 100644
--- a/src/smt/nseq_context_solver.h
+++ b/src/smt/nseq_context_solver.h
@@ -88,6 +88,10 @@ namespace smt {
             return m_arith_value.get_up(e, hi, is_strict) && !is_strict && hi.is_int();
         }
 
+        bool current_value(expr* e, rational& v) const override {
+            return m_arith_value.get_value(e, v) && v.is_int(); 
+        }            
+
         lbool check_with_assumptions(expr_ref_vector& assumptions, expr_ref_vector& core) override {
             // TODO: Not ideal
             // Replay with assumptions
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index a057c587e..99f679798 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -284,6 +284,8 @@ namespace seq {
         // Default implementation reports "unsupported".
         virtual bool    lower_bound(expr* e, rational& lo) const { return false; }
         virtual bool    upper_bound(expr* e, rational& hi) const { return false; }
+        virtual bool current_value(expr *e, rational &v) const { return false; }
+        
         virtual void    reset() = 0;
     };