From 9bd8fb60926ac2589a6f8930350f787d5579c2e5 Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <ahmed.irfan@sri.com>
Date: Tue, 1 Oct 2024 18:02:26 -0700
Subject: [PATCH] check cached value if it must be decided

---
 src/mcsat/nra/nra_plugin.c | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c
index fca8c4e2d..4b5693c98 100644
--- a/src/mcsat/nra/nra_plugin.c
+++ b/src/mcsat/nra/nra_plugin.c
@@ -1130,10 +1130,14 @@ void nra_plugin_decide(plugin_t* plugin, variable_t x, trail_token_t* decide_tok
   // Decide if not too complex of a rational number
   bool decide = true;
   if (!must) {
-    if (!lp_value_is_rational(&x_new_lpvalue)) {
-      if (lp_upolynomial_degree(x_new_lpvalue.value.a.f) > 2) {
+    if (using_cached) {
+      if (!lp_value_is_rational(&x_cached_value->lp_value) &&
+          lp_upolynomial_degree(x_cached_value->lp_value.value.a.f) > 2) {
         decide = false;
       }
+    } else if (!lp_value_is_rational(&x_new_lpvalue) &&
+               lp_upolynomial_degree(x_new_lpvalue.value.a.f) > 2) {
+      decide = false;
     }
   }