diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index ac2cb843c..4aeda7a5c 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -41,18 +41,12 @@ Revision History:
 // -----------------------------------
 
 parameter::~parameter() {
-    if (auto p = std::get_if<rational*>(&m_val)) {
-        dealloc(*p);
-    }
     if (auto p = std::get_if<zstring*>(&m_val)) {
         dealloc(*p);
     }
 }
 
 parameter::parameter(parameter const& other) : m_val(other.m_val) {
-    if (auto p = std::get_if<rational*>(&m_val)) {
-        m_val = alloc(rational, **p);
-    }
     if (auto p = std::get_if<zstring*>(&m_val)) {
         m_val = alloc(zstring, **p);
     }
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 3f194f0d3..6e5ce8c78 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -123,7 +123,7 @@ private:
         ast*,      // for PARAM_AST
         symbol,    // for PARAM_SYMBOL
         zstring*,  // for PARAM_ZSTRING
-        rational*, // for PARAM_RATIONAL
+        rational,  // for PARAM_RATIONAL
         double,    // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin)
         unsigned   // for PARAM_EXTERNAL
     > m_val = 0;
@@ -135,8 +135,8 @@ public:
     explicit parameter(unsigned val): m_val((int)val) {}
     explicit parameter(ast * p): m_val(p) {}
     explicit parameter(symbol const & s): m_val(s) {}
-    explicit parameter(rational const & r): m_val(alloc(rational, r)) {}
-    explicit parameter(rational && r) : m_val(alloc(rational, std::move(r))) {} 
+    explicit parameter(rational const & r): m_val(r) {}
+    explicit parameter(rational && r) : m_val(std::move(r)) {} 
     explicit parameter(zstring const& s): m_val(alloc(zstring, s)) {}
     explicit parameter(zstring && s): m_val(alloc(zstring, std::move(s))) {}
     explicit parameter(double d): m_val(d) {}
@@ -188,7 +188,7 @@ public:
     int get_int() const { SASSERT(is_int()); return std::get<int>(m_val); }
     ast * get_ast() const { SASSERT(is_ast()); return std::get<ast*>(m_val); }
     symbol get_symbol() const { SASSERT(is_symbol()); return std::get<symbol>(m_val); }
-    rational const & get_rational() const { SASSERT(is_rational()); return *std::get<rational*>(m_val); }
+    rational const & get_rational() const { SASSERT(is_rational()); return std::get<rational>(m_val); }
     zstring const& get_zstring() const { SASSERT(is_zstring()); return *std::get<zstring*>(m_val); }
     double get_double() const { SASSERT(is_double()); return std::get<double>(m_val); }
     unsigned get_ext_id() const { SASSERT(is_external()); return std::get<unsigned>(m_val); }