From 75d1e8e9295d74f64e912c675a2c6317de68f644 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 28 Jan 2020 12:06:56 -0800
Subject: [PATCH] return l_undef in get_phase() if lpvar is not available

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 4492c69f0..386166a3c 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1075,6 +1075,8 @@ public:
             break;
         }         
         auto vi = get_lpvar(b->get_var());
+        if (vi == lp::null_lpvar)
+            return l_undef;
         return m_solver->compare_values(vi, k, b->get_value()) ? l_true : l_false;
     }