diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index c0c62c379..4524b7f15 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -33,6 +33,8 @@ Revision History:
 #include "ast/fpa_decl_plugin.h"
 #include "ast/for_each_ast.h"
 #include "ast/decl_collector.h"
+#include "math/polynomial/algebraic_numbers.h"
+
 
 // ---------------------------------------
 // smt_renaming
@@ -372,6 +374,12 @@ class smt_printer {
                 display_rational(val, is_int);
             }
         }
+        else if (m_autil.is_irrational_algebraic_numeral(n)) {
+            anum const & aval = m_autil.to_irrational_algebraic_numeral(n);
+            std::ostringstream buffer;
+            m_autil.am().display_root_smt2(buffer, aval);            
+            m_out << buffer.str();
+        }
         else if (m_sutil.str.is_string(n, s)) {
             std::string encs = s.encode();
             m_out << "\"";