Evaluate cast-to-real operator (#7599)

Fixes cvc5/cvc5-projects#341.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 2d6c3de55..f7c5ddf0f 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -491,6 +491,13 @@ EvalResult Evaluator::evalInternal(
           results[currNode] = EvalResult(x.abs());
           break;
         }
+        case kind::CAST_TO_REAL:
+        {
+          // casting to real is a no-op
+          const Rational& x = results[currNode[0]].d_rat;
+          results[currNode] = EvalResult(x);
+          break;
+        }
         case kind::CONST_STRING:
           results[currNode] = EvalResult(currNodeVal.getConst<String>());
           break;