diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index b9d41cec9..ed05dd498 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1473,6 +1473,12 @@ namespace polysat {
         return r.is_val();
     }
 
+    rational solver::eval(pdd const& p) const {
+        rational r;
+        VERIFY(try_eval(p, r));
+        return r;
+    }
+
     /**
      * Variable activity accounting.
      * As a placeholder we increment activity
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 00669a44c..046ce20d3 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -415,6 +415,7 @@ namespace polysat {
          * Evaluate term under the current assignment.
          */
         bool try_eval(pdd const& p, rational& out_value) const;
+        rational eval(pdd const& p) const;
 
         /**
          * Add variable with bit-size.