fix #3542

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/sat_solver/inc_sat_solver.cpp

@@ -222,7 +222,17 @@ public:
     }
 
     void push() override {
-        internalize_formulas();
+        try {
+            internalize_formulas();
+        }
+        catch (...) {
+            push_internal();
+            throw;
+        }
+        push_internal();
+    }
+
+    void push_internal() {
         m_solver.user_push();
         ++m_num_scopes;
         m_mcs.push_back(m_mcs.back());
@@ -599,6 +609,11 @@ private:
             m_bb_rewriter = nullptr;
             return l_undef;
         }        
+        catch (...) {
+            m_preprocess = nullptr;
+            m_bb_rewriter = nullptr;
+            throw;
+        }
         if (m_subgoals.size() != 1) {
             IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n");
             return l_undef;

src/smt/theory_diff_logic_def.h

@@ -921,7 +921,7 @@ template<typename Ext>
 bool theory_diff_logic<Ext>::is_consistent() const {
     DEBUG_CODE(
         context& ctx = get_context();
-        for (unsigned i = 0; i < m_atoms.size(); ++i) {
+        for (unsigned i = 0; m_graph.is_feasible() && i < m_atoms.size(); ++i) {
             atom* a = m_atoms[i];
             bool_var bv = a->get_bool_var();
             lbool asgn = ctx.get_assignment(bv);