Fixed a failing datatype regression with check-models

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 452317f5b13d16d48a1547eed923bc036834e82d..957491d37c424336f3f0bfcde2843be8daaec103 100644 (file)
--- 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);
 }