diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 1bd495a87..042cdde6f 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -4582,7 +4582,7 @@ def SetIntersect(*args):
     >>> a = Const('a', SetSort(IntSort()))
     >>> b = Const('b', SetSort(IntSort()))
     >>> SetIntersect(a, b)
-    intersect(a, b)
+    intersection(a, b)
     """
     args = _get_args(args)
     ctx = _ctx_from_ast_arg_list(args)
@@ -4623,7 +4623,7 @@ def SetDifference(a, b):
     >>> a = Const('a', SetSort(IntSort()))
     >>> b = Const('b', SetSort(IntSort()))
     >>> SetDifference(a, b)
-    difference(a, b)
+    setminus(a, b)
     """
     ctx = _ctx_from_ast_arg_list([a, b])
     return ArrayRef(Z3_mk_set_difference(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index b43147c33..7ca2c774b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1116,7 +1116,9 @@ namespace opt {
         val = (*mdl)(term);
         unsigned bvsz;
         if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bvsz)) {
-            TRACE("opt", tout << "model does not evaluate objective to a value\n";);
+            TRACE("opt", tout << "model does not evaluate objective to a value but instead " << val << "\n";
+                  tout << *mdl << "\n";
+                  );
             return false;
         }
         if (r != v) {