From e3b1ce1fdc24baf10be47ef760393c384c518c23 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@hotmail.com>
Date: Wed, 27 May 2015 10:07:09 -0700
Subject: [PATCH] also allw n-ary distrinct

Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
---
 examples/tptp/tptp5.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index 63971a7d9..3b8d2364d 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -809,8 +809,12 @@ class env {
                 r = terms[0] / terms[1];
             }
             else if (!strcmp(ch,"$distinct")) {
-                check_arity(terms.size(), 2);
-                r = terms[0] != terms[1];
+                if (terms.size() == 2) {
+                    r = terms[0] != terms[1];
+                }
+                else {
+                    r = distinct(terms);
+                }
             }
             else if (!strcmp(ch,"$floor") || !strcmp(ch,"$to_int")) {
                 check_arity(terms.size(), 1);