diff --git a/src/duality/duality.h b/src/duality/duality.h
index fc70ffa70..1445bc881 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -253,6 +253,10 @@ protected:
         }
 
         void assert_axiom(const expr &axiom){
+	  // HACK: large "distict" predicates can kill the legacy SMT solver -- ignore them
+	  if(axiom.is_app() && axiom.decl().get_decl_kind() == Distinct)
+	    if(axiom.num_args() > 10)
+	      return;
             islvr->AssertInterpolationAxiom(axiom);
         }