From 60ef669fbc8b3fd3a1aaa10e179c2edee41eadbe Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Thu, 10 Apr 2014 17:54:49 -0700
Subject: [PATCH] removed distinct predicate hack

---
 src/duality/duality.h | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/duality/duality.h b/src/duality/duality.h
index 1445bc881..572ce427b 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -253,10 +253,12 @@ protected:
         }
 
         void assert_axiom(const expr &axiom){
+#if 0
 	  // 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;
+#endif
             islvr->AssertInterpolationAxiom(axiom);
         }