From e2f2708a9c4f09d38ea0cc5fa98c9ad59f2a94ec Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 19 Oct 2015 21:12:43 +0100
Subject: [PATCH] Fixed array default operator

---
 src/api/python/z3.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 3b869d1fd..68f559635 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -4064,7 +4064,7 @@ def Default(a):
     """  
     if __debug__:  
         _z3_assert(is_array(a), "First argument must be a Z3 array expression")  
-    return a.mk_default()  
+    return a.default()  
 
 
 def Store(a, i, v):