From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 26 Oct 2012 19:54:06 +0000 (+0000)
Subject: Fixed a failing datatype regression with check-models
X-Git-Tag: cvc5-1.0.0~7666
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=634b155b5716a72716836193466aac9df5ad649d;p=cvc5.git

Fixed a failing datatype regression with check-models
---

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);
 }