From 68c086c5896cd496c83956b3b1211287dab1c455 Mon Sep 17 00:00:00 2001
From: vhalros <vhalros@gmail.com>
Date: Fri, 24 Jul 2015 15:24:23 -0400
Subject: [PATCH] Added default operator to array interface.

---
 src/api/python/z3.py | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index ce1cc2103..34e1d2645 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -3906,6 +3906,12 @@ class ArrayRef(ExprRef):
         arg = self.domain().cast(arg)
         return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
 
+    def default(self):
+	return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx)
+
+
+
+
 def is_array(a):
     """Return `True` if `a` is a Z3 array expression.