mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #3543

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-04 21:56:46 -07:00
parent 0fc8ebc8cc
commit 2f80acb1bc
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_diff_logic_def.h
View file

@ -359,6 +359,8 @@ final_check_status theory_diff_logic<Ext>::final_check_eh() {
} }
TRACE("arith_final", display(tout); ); TRACE("arith_final", display(tout); );
if (!is_consistent())
return FC_CONTINUE;
SASSERT(is_consistent()); SASSERT(is_consistent());
if (m_non_diff_logic_exprs) { if (m_non_diff_logic_exprs) {
return FC_GIVEUP; return FC_GIVEUP;