Merge branch 'unstable' of https://git01.codeplex.com/z3 into opt

src/api/c++/z3++.h

@@ -652,6 +652,8 @@ namespace z3 {
             return expr(c.ctx(), r);
         }
 
+        friend expr distinct(expr_vector const& args);
+
         friend expr operator==(expr const & a, expr const & b) {
             check_context(a, b);
             Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
@@ -1065,6 +1067,16 @@ namespace z3 {
         array<Z3_app> vars(xs);  
         Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r);
     }
+
+
+    inline expr distinct(expr_vector const& args) {
+        assert(args.size() > 0);
+        context& ctx = args[0].ctx();
+        array<Z3_ast> _args(args);
+        Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
+        ctx.check_error();
+        return expr(ctx, r);
+    }
     
     class func_entry : public object {
         Z3_func_entry m_entry;

src/api/dotnet/Context.cs

@@ -916,6 +916,8 @@ namespace Microsoft.Z3
             CheckContextMatch(t);
             return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
+
+
         #endregion
 
         #region Arithmetic

src/api/dotnet/Expr.cs

@@ -320,6 +320,7 @@ namespace Microsoft.Z3
         /// Indicates whether the term is an implication
         /// </summary>
         public bool IsImplies { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
+
         #endregion
 
         #region Arithmetic Terms