summaryrefslogtreecommitdiff
path: root/src/theory/valuation.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/valuation.cpp')
-rw-r--r--src/theory/valuation.cpp8
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback