diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index dde9ba86f..00a647474 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -797,6 +797,23 @@ namespace z3 {
             assert(is_numeral() || is_algebraic());
             return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
         }
+
+        /**
+         * Retrieve lower and upper bounds for algebraic numerals based on a decimal precision
+         */
+        expr algebraic_lower(unsigned precision) const { 
+            assert(is_algebraic());      
+            Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
+            check_error();
+            return expr(ctx(), r);
+        }
+
+        expr algebraic_upper(unsigned precision) const { 
+            assert(is_algebraic());      
+            Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
+            check_error();
+            return expr(ctx(), r);
+        }
         
 
         /**
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 8167d6b40..10fb7836e 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3364,10 +3364,13 @@ namespace smt {
             r = l_undef;
         }
         if (r == l_true && gparams::get_value("model_validate") == "true") {
-            model_ref mdl;
-            get_model(mdl);
-            for (theory* t : m_theory_set) {
-                t->validate_model(*mdl);
+            recfun::util u(m);
+            if (u.get_rec_funs().empty()) {
+                model_ref mdl;
+                get_model(mdl);
+                for (theory* t : m_theory_set) {
+                    t->validate_model(*mdl);
+                }
             }
 #if 0
             for (literal lit : m_assigned_literals) {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 8fee8fe3c..6351b84de 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -4412,6 +4412,7 @@ app* theory_seq::mk_value(app* e) {
 
 
 void theory_seq::validate_model(model& mdl) {
+    return;
     for (auto const& eq : m_eqs) {
         expr_ref_vector ls = eq.ls();
         expr_ref_vector rs = eq.rs();