fix #2787

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

1 files changed, 11 insertions, 2 deletions

diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 1e961d1..d85ba9d 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -359,13 +359,22 @@ final_check_status theory_diff_logic<Ext>::final_check_eh() {
     }
 
     TRACE("arith_final", display(tout); );
-    // either will already be zero (as we don't do mixed constraints).
-    m_graph.set_to_zero(get_zero(true), get_zero(false));
     SASSERT(is_consistent());
     if (m_non_diff_logic_exprs) {
         return FC_GIVEUP; 
     }
 
+    for (enode* n : get_context().enodes()) {
+        family_id fid = n->get_owner()->get_family_id();
+        if (fid != get_family_id() && 
+            fid != get_manager().get_basic_family_id()) {
+            return FC_GIVEUP;
+        }
+    }
+    
+    // either will already be zero (as we don't do mixed constraints).
+    m_graph.set_to_zero(get_zero(true), get_zero(false));
+
     return FC_DONE;
 }