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