From 17bcb37cf1f0560a6af8a2bed3bc1d6ec6bb77fb Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 8 Nov 2017 20:09:09 +0000
Subject: [PATCH] Fixed error handlers in Python API.

---
 scripts/update_api.py   | 20 ++++++++++++--------
 src/api/python/z3/z3.py | 15 ++++++++-------
 2 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/scripts/update_api.py b/scripts/update_api.py
index 7d43b70ce..2828a63f8 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -324,14 +324,16 @@ class Elementaries:
     self.OK = Z3_OK
     self.Exception = Z3Exception
 
-  def Check(self, ctx): 
+  def Check(self, ctx):
     err = self.get_error_code(ctx)
     if err != self.OK:
         raise self.Exception(self.get_error_message(ctx, err))
 
 def Z3_set_error_handler(ctx, hndlr, _elems=Elementaries(_lib.Z3_set_error_handler)):
-  _elems.f(ctx, ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)(hndlr))
+  ceh = _error_handler_type(hndlr)
+  _elems.f(ctx, ceh)
   _elems.Check(ctx)
+  return ceh
 
 """)
 
@@ -1637,10 +1639,10 @@ from .z3consts import *
 
 _ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
 _lib = None
-_default_dirs = ['.', 
-                 os.path.dirname(os.path.abspath(__file__)), 
-                 pkg_resources.resource_filename('z3', 'lib'), 
-                 os.path.join(sys.prefix, 'lib'),                  
+_default_dirs = ['.',
+                 os.path.dirname(os.path.abspath(__file__)),
+                 pkg_resources.resource_filename('z3', 'lib'),
+                 os.path.join(sys.prefix, 'lib'),
                  None]
 _all_dirs = []
 
@@ -1667,7 +1669,7 @@ for d in _all_dirs:
     if os.path.isdir(d):
       d = os.path.join(d, 'libz3.%s' % _ext)
       if os.path.isfile(d):
-        _lib = ctypes.CDLL(d)              
+        _lib = ctypes.CDLL(d)
         break
   except:
     pass
@@ -1710,8 +1712,10 @@ else:
      else:
         return ""
 
+_error_handler_type  = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
+
 _lib.Z3_set_error_handler.restype  = None
-_lib.Z3_set_error_handler.argtypes = [ContextObj, ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)]
+_lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
 
 """
   )
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 21ac695db..a247d0a3a 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -125,11 +125,6 @@ def _get_args(args):
     except:  # len is not necessarily defined when args is not a sequence (use reflection?)
         return args
 
-def z3_error_handler(c, e):
-    # Do nothing error handler, just avoid exit(0)
-    # The wrappers in z3core.py will raise a Z3Exception if an error is detected
-    return
-
 def _to_param_value(val):
     if isinstance(val, bool):
         if val == True:
@@ -139,6 +134,11 @@ def _to_param_value(val):
     else:
         return str(val)
 
+def z3_error_handler(c, e):
+    # Do nothing error handler, just avoid exit(0)
+    # The wrappers in z3core.py will raise a Z3Exception if an error is detected
+    return
+
 class Context:
     """A Context manages all other Z3 objects, global configuration options, etc.
 
@@ -165,13 +165,14 @@ class Context:
                 Z3_set_param_value(conf, str(prev), _to_param_value(a))
                 prev = None
         self.ctx = Z3_mk_context_rc(conf)
+        self.eh = Z3_set_error_handler(self.ctx, z3_error_handler)
         Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
-        Z3_set_error_handler(self.ctx, z3_error_handler)
         Z3_del_config(conf)
 
     def __del__(self):
-        Z3_del_context(self.ctx)
+        Z3_del_context(self.ctx)        
         self.ctx = None
+        self.eh = None
 
     def ref(self):
         """Return a reference to the actual C pointer to the Z3 context."""