diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp
index 3bb33638f..38f0289e6 100644
--- a/src/api/api_algebraic.cpp
+++ b/src/api/api_algebraic.cpp
@@ -150,6 +150,7 @@ extern "C" {
                 r = au(c).mk_numeral(_r, false);                        \
             }                                                           \
         }                                                               \
+        mk_c(c)->save_ast_trail(r);                                     \
         RETURN_Z3(of_ast(r));
 
 
@@ -222,6 +223,7 @@ extern "C" {
             _am.root(av, k, _r);
         }
         expr * r = au(c).mk_numeral(_r, false);
+        mk_c(c)->save_ast_trail(r);
         RETURN_Z3(of_ast(r));
         Z3_CATCH_RETURN(0);
     }
@@ -243,6 +245,7 @@ extern "C" {
             _am.power(av, k, _r);
         }
         expr * r = au(c).mk_numeral(_r, false);
+        mk_c(c)->save_ast_trail(r);
         RETURN_Z3(of_ast(r));
         Z3_CATCH_RETURN(0);
     }
diff --git a/src/util/basic_interval.h b/src/util/basic_interval.h
index 2bf5a8f30..ef414149c 100644
--- a/src/util/basic_interval.h
+++ b/src/util/basic_interval.h
@@ -260,8 +260,8 @@ public:
        \brief c <- a - b
     */
     void sub(interval const & a, interval const & b, interval & c) {
-        m().sub(a.m_lower, b.m_lower, c.m_lower);
-        m().sub(a.m_upper, b.m_upper, c.m_upper);
+        m().sub(a.m_lower, b.m_upper, c.m_lower);
+        m().sub(a.m_upper, b.m_lower, c.m_upper);
     }
 
 private: