diff --git a/src/ast/ast.h b/src/ast/ast.h index 364be8a77..89df04961 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -122,6 +122,7 @@ public: explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {} explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s.c_ptr()) {} explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(alloc(rational, r)) {} + explicit parameter(rational && r) : m_kind(PARAM_RATIONAL), m_rational(alloc(rational, std::move(r))) {} explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {} explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s).c_ptr()) {} explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}