diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 6233de937..37f9cf7f8 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -359,6 +359,8 @@ final_check_status theory_diff_logic::final_check_eh() { } TRACE("arith_final", display(tout); ); + if (!is_consistent()) + return FC_CONTINUE; SASSERT(is_consistent()); if (m_non_diff_logic_exprs) { return FC_GIVEUP;