diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-10-26 19:24:09 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-10-26 19:24:09 +0000 |
| commit | 118b6163f42af017a5ea7f9229df0a9e584c0050 (patch) | |
| tree | 2f840f4ccfed6a616db8dfd063936e0134146e18 | |
| parent | f4969cca302fe640fed334cf9cbf8e032b468ae6 (diff) | |
GetValueCommand now gives a TUPLE as output, with the first operand the input expression and the second the value (resolves bug 227)
| -rw-r--r-- | src/expr/command.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 38193a75b..60b48542b 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -269,7 +269,8 @@ GetValueCommand::GetValueCommand(Expr term) : } void GetValueCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->getValue(d_term); + d_result = d_term.getExprManager()->mkExpr(kind::TUPLE, d_term, + smtEngine->getValue(d_term)); } Expr GetValueCommand::getResult() const { |