diff --git a/scripts/update_api.py b/scripts/update_api.py
index e97c32be8..3c1e1cc07 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -321,6 +321,7 @@ def mk_py_wrappers():
         core_py.write("def %s(" % name)
         display_args(num)
         core_py.write("):\n")
+        core_py.write("  _lib = lib()\n")
         core_py.write("  if _lib.%s is None:\n" % name)
         core_py.write("     return\n")
         if result != VOID:
@@ -1604,16 +1605,7 @@ def write_exe_c_preamble(exe_c):
 
 def write_core_py_post(core_py):
   core_py.write("""
-_dirs = ['.', os.path.dirname(os.path.abspath(__file__)), pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
 
-for _dir in _dirs:
-   try:
-      init(_dir)
-      break
-   except:
-      pass
-if _lib is None:
-    raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
 """)
     
 def write_core_py_preamble(core_py):
@@ -1631,6 +1623,16 @@ _lib = None
 
 def lib():
   global _lib
+  if _lib is None:
+     _dirs = ['.', os.path.dirname(os.path.abspath(__file__)), pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
+     for _dir in _dirs:
+       try:
+          init(_dir)
+          break
+       except:
+          pass
+  if _lib is None:
+    raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
   return _lib
 
 def _to_ascii(s):
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 89e0123a8..13f8ab282 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1549,14 +1549,12 @@ namespace smt {
         expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m);
 
         expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m);
+        assert_axiom(breakdownAssert);
+        
         SASSERT(breakdownAssert);
 
         expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m);
-        SASSERT(reduceToResult);
-
-        expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToResult), m);
-        SASSERT(finalAxiom);
-        assert_axiom(finalAxiom);
+        assert_axiom(reduceToResult);
     }
 
     void theory_str::instantiate_axiom_str_to_int(enode * e) {