diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 568ffe9a2..b4cdf834b 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6194,7 +6194,7 @@ class Solver(Z3PPObject):
         >>> s.consequences([a],[b,c,d])
         (sat, [Implies(a, b), Implies(a, c)])
         >>> s.consequences([Not(c),d],[a,b,c,d])
-        (sat, [Implies(Not(c), Not(c)), Implies(d, d), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
+        (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
         """
         if isinstance(assumptions, list):
             _asms = AstVector(None, self.ctx)
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index af3c57baa..1310727aa 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1235,7 +1235,7 @@ namespace opt {
             out << " (";
             display_objective(out, obj);
             if (get_lower_as_num(i) != get_upper_as_num(i)) {
-                out << "  (" << get_lower(i) << " " << get_upper(i) << ")";
+                out << "  (interval " << get_lower(i) << " " << get_upper(i) << ")";
             }
             else {
                 out << " " << get_lower(i);