From 20d8fe633c1f113dceade2df232a35db03e6288c Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 8 Nov 2021 12:57:12 -0600
Subject: [PATCH] Evaluate cast-to-real operator (#7599)

Fixes cvc5/cvc5-projects#341.
---
 src/theory/evaluator.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

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;
-- 
2.30.2