Fix bug reported at http://stackoverflow.com/questions/13923316/unprintable-solver-model

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

RELEASE_NOTES

@@ -45,6 +45,8 @@ Version 4.3.2
       unsat
   We say may because 'F' may have other unsatisfiable cores.
 
+- Fixed bug reported at http://stackoverflow.com/questions/13923316/unprintable-solver-model
+
 Version 4.3.1
 =============
 

src/api/python/z3.py

@@ -5122,7 +5122,10 @@ class FuncInterp(Z3PPObject):
             Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
 
     def else_value(self):
-        """Return the `else` value for a function interpretation.
+        """
+        Return the `else` value for a function interpretation.
+        Return None if Z3 did not specify the `else` value for
+        this object.
 
         >>> f = Function('f', IntSort(), IntSort())
         >>> s = Solver()
@@ -5135,7 +5138,11 @@ class FuncInterp(Z3PPObject):
         >>> m[f].else_value()
         1
         """
-        return _to_expr_ref(Z3_func_interp_get_else(self.ctx.ref(), self.f), self.ctx)
+        r = Z3_func_interp_get_else(self.ctx.ref(), self.f)
+        if r:
+            return _to_expr_ref(r, self.ctx)
+        else:
+            return None
 
     def num_entries(self):
         """Return the number of entries/points in the function interpretation `self`.

src/api/python/z3printer.py

@@ -791,7 +791,11 @@ class Formatter:
                 r.append(self.pp_ellipses())
                 break
         if sz <= self.max_args:
-            else_pp = self.pp_expr(f.else_value(), 0, [])
+            else_val = f.else_value()
+            if else_val == None:
+                else_pp  = to_format('#unspecified')
+            else:
+                else_pp  = self.pp_expr(else_val, 0, [])
             r.append(group(seq((to_format('else'), else_pp), self.pp_arrow())))
         return seq3(r, '[', ']')