1 files changed, 3 insertions, 5 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 847221979..f8e28a994 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1408,12 +1408,10 @@ void GetValueCommand::invoke(SmtEngine* smtEngine)
       Node value = Node::fromExpr(smtEngine->getValue(e));
       if (value.getType().isInteger() && request.getType() == nm->realType())
       {
-        // Need to wrap in special marker so that output printers know this
+        // Need to wrap in division-by-one so that output printers know this
         // is an integer-looking constant that really should be output as
-        // a rational.  Necessary for SMT-LIB standards compliance, but ugly.
-        value = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
-                           nm->mkConst(AscriptionType(em->realType())),
-                           value);
+        // a rational.  Necessary for SMT-LIB standards compliance.
+        value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1)));
       }
       result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr());
     }