diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 11:19:48 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 15:12:51 -0400 |
commit | 65f0dc22fe49c6c388e9413f3b7541d7fb49a3b3 (patch) | |
tree | 2601c6cb44feda628dfd001e83f5030ff69dc3f8 /src/expr | |
parent | 4fb42ac1e5a96c1633bb4570681b09db657f673d (diff) |
Fix output of integer-valued real constants in SMT-LIB models (thanks Christoph Sticksel for reporting).
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 16484a320..69bdd704b 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -896,6 +896,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); |