summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3a4fd90e9..5de1cd0b1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -410,7 +410,7 @@ Expr SmtEngine::getValue(Expr e)
Node resultNode = d_theoryEngine->getValue(n);
// type-check the result we got
- Assert(resultNode.getType(true) == eNode.getType());
+ Assert(resultNode.isNull() || resultNode.getType(true) == eNode.getType());
return Expr(d_exprManager, new Node(resultNode));
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback