diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 15:15:45 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 15:15:45 -0400 |
commit | 9323af51596eece5107b6ee4f7423ad56c9385b8 (patch) | |
tree | 65675635487223e5e679dd49cf8703ae1752ef19 /src/expr | |
parent | 6294adeb83155c54539b2d2d31fa9e3a5b6f1a00 (diff) | |
parent | 65f0dc22fe49c6c388e9413f3b7541d7fb49a3b3 (diff) |
Merge branch '1.4.x'
Conflicts:
NEWS
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index a3f5170fa..4d9ca9f30 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -899,6 +899,13 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { smt::SmtScope scope(smtEngine); Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i); Node value = Node::fromExpr(smtEngine->getValue(*i)); + if(value.getType().isInteger() && request.getType() == nm->realType()) { + // Need to wrap in special marker 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); + } result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr()); } d_result = em->mkExpr(kind::SEXPR, result); |