summaryrefslogtreecommitdiff
path: root/src/theory/model.cpp
diff options
context:
space:
mode:
authorClark Barrett <barrett@cs.nyu.edu>2012-10-26 02:37:38 +0000
committerClark Barrett <barrett@cs.nyu.edu>2012-10-26 02:37:38 +0000
commitddd3797ee72443bd35f6cea146c3752ea0dd2286 (patch)
treeda5f69ec295e31eddcca999247f98025bd8e5752 /src/theory/model.cpp
parent20897efe113ff62e5a91840933a0b424e32f6771 (diff)
More bug fixes and more checks for models
Diffstat (limited to 'src/theory/model.cpp')
-rw-r--r--src/theory/model.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index aa2de656e..452317f5b 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -75,6 +75,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
}
Node TheoryModel::getModelValue( TNode n ) const{
+ Assert(n.getKind() != kind::FORALL && n.getKind() != kind::EXISTS && n.getKind() != kind::LAMBDA);
if( n.isConst() ) {
return n;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback