diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-26 19:54:06 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-26 19:54:06 +0000 |
| commit | 634b155b5716a72716836193466aac9df5ad649d (patch) | |
| tree | fa56a510bdd44ecb0fc7767c592a7f56bf8b523e /src/theory/model.cpp | |
| parent | dbaaa9f285a2bcb5fd7a555e753968972b998f15 (diff) | |
Fixed a failing datatype regression with check-models
Diffstat (limited to 'src/theory/model.cpp')
| -rw-r--r-- | src/theory/model.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 452317f5b..957491d37 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -360,7 +360,7 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t bool TheoryEngineModelBuilder::isAssignable(TNode n) { - return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT); + return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR); } |