diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-31 18:35:45 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-31 18:35:45 +0000 |
commit | ceca24424da629db2e133f7864b0bac03ad44829 (patch) | |
tree | 6b50c8337f6617ee11718cede5fbaf35a21d6a6c /src/theory/valuation.cpp | |
parent | b04d7ee960729bcde8677be3682a2d64789f825b (diff) |
Fixes to Valuation.
Diffstat (limited to 'src/theory/valuation.cpp')
-rw-r--r-- | src/theory/valuation.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 1f82f1404..9f33c2c4f 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -29,7 +29,13 @@ Node Valuation::getValue(TNode n) { Node Valuation::getSatValue(TNode n) { if(n.getKind() == kind::NOT) { - return NodeManager::currentNM()->mkConst(! d_engine->getPropEngine()->getValue(n[0]).getConst<bool>()); + Node atomRes = d_engine->getPropEngine()->getValue(n[0]); + if(atomRes.getKind() == kind::CONST_BOOLEAN){ + return NodeManager::currentNM()->mkConst(!atomRes.getConst<bool>()); + }else{ + Assert(atomRes.isNull()); + return atomRes; + } } else { return d_engine->getPropEngine()->getValue(n); } |