From 2c078b01dacd8b06ee58d40030810cc1b0244e69 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 Mar 2020 16:56:26 -0700
Subject: [PATCH] fix #3422

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_solver/inc_sat_solver.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 5124ca586..cd679047b 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -876,6 +876,10 @@ private:
             mdl = nullptr;
             return;
         }
+        if (m_fmls.size() > m_fmls_head) {
+            mdl = nullptr;
+            return;
+        }
         TRACE("sat", m_solver.display_model(tout););
         CTRACE("sat", m_sat_mc, m_sat_mc->display(tout););
         sat::model ll_m = m_solver.get_model();