From 1949a978ceed23e849e3eb1d6c237e19ac7f22ab Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Apr 2020 11:39:25 -0700
Subject: [PATCH] fix #3760

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

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 3daf26976..f7f663da8 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1152,6 +1152,8 @@ namespace sat {
                 }
                 literal l(v, false);
                 if (mdl[v] != l_true) l.neg();
+                if (inconsistent())
+                    return l_undef;
                 push();
                 assign_core(l, justification(scope_lvl()));
                 propagate(false);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 1dcdfbf0a..b40a59a00 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -380,6 +380,8 @@ public:
             }
         }
         convert_internalized();
+        if (m_solver.inconsistent())
+            return last_cube(false);
         obj_hashtable<expr> _vs;
         for (expr* v : vs) _vs.insert(v);
         sat::bool_var_vector vars;