From ced665eb46721657c57b391571ce76768d4f4779 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 14 Jun 2018 09:20:47 -0700
Subject: Fix CONST_RATIONAL conversion in evaluation

---
 src/theory/evaluator.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 55d454d89..019ca86d5 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -103,8 +103,7 @@ EvalResult Evaluator::evalInternal(TNode n,
         case kind::CONST_RATIONAL:
         {
           const Rational& r = currNodeVal.getConst<Rational>();
-          Assert(r.getDenominator() == 1);
-          results[currNode] = EvalResult(r.getNumerator());
+          results[currNode] = EvalResult(r);
           break;
         }
 
-- 
cgit v1.2.3