From 4b8a063996dfe2bdbdca6ffa6d2bcf568dea86a5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 21 Mar 2020 18:11:04 -0700
Subject: [PATCH] convert seg fault to assertion violation #3456

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/emonics.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index 9079c7c01..84d95d40b 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -555,6 +555,8 @@ bool emonics::invariant() const {
     std::function<bool(lpvar, unsigned)> find_index = [&,this](lpvar v, unsigned idx) {
         cell* c = m_use_lists[v].m_head;
         cell* c0 = c;
+        if (!c)
+            return false;
         bool found = false;
         do {
             found |= c->m_index == idx;