Evaluate cast-to-real operator (#7599)

Fixes cvc5/cvc5-projects#341.

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 2d6c3de55c50e3e399d9869841bbe71500fe3dd0..f7c5ddf0f2dd68908eb42b87a251014b6f06dbe1 100644 (file)
--- 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;