From cd6e11c2887a71f559ab2e278ec944246c346c04 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 31 Jul 2019 11:01:33 -0500
Subject: [PATCH] Add some missing cases in evaluator (#3133)

---
 src/theory/evaluator.cpp | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 818f40e8c..ffb5b9fd4 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -259,6 +259,12 @@ EvalResult Evaluator::evalInternal(TNode n,
           break;
         }
 
+        case kind::UMINUS:
+        {
+          const Rational& x = results[currNode[0]].d_rat;
+          results[currNode] = EvalResult(-x);
+          break;
+        }
         case kind::MULT:
         {
           Rational res = results[currNode[0]].d_rat;
@@ -277,6 +283,27 @@ EvalResult Evaluator::evalInternal(TNode n,
           results[currNode] = EvalResult(x >= y);
           break;
         }
+        case kind::LEQ:
+        {
+          const Rational& x = results[currNode[0]].d_rat;
+          const Rational& y = results[currNode[1]].d_rat;
+          results[currNode] = EvalResult(x <= y);
+          break;
+        }
+        case kind::GT:
+        {
+          const Rational& x = results[currNode[0]].d_rat;
+          const Rational& y = results[currNode[1]].d_rat;
+          results[currNode] = EvalResult(x > y);
+          break;
+        }
+        case kind::LT:
+        {
+          const Rational& x = results[currNode[0]].d_rat;
+          const Rational& y = results[currNode[1]].d_rat;
+          results[currNode] = EvalResult(x < y);
+          break;
+        }
 
         case kind::CONST_STRING:
           results[currNode] = EvalResult(currNodeVal.getConst<String>());
-- 
2.30.2