Minor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.

1 files changed, 7 insertions, 1 deletions

diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index a5a78e691..e2830b57e 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -116,7 +116,13 @@ struct MemberTypeRule {
       }
       TypeNode elementType = n[0].getType(check);
       if(!elementType.isComparableTo(setType.getSetElementType())) {
-        throw TypeCheckingExceptionPrivate(n, "member operating on sets of different types");
+      //if(!elementType.isSubtypeOf(setType.getSetElementType())) {     //FIXME:typing
+        std::stringstream ss;
+        ss << "member operating on sets of different types:\n"
+           << "child type:  " << elementType << "\n"
+           << "not subtype: " << setType.getSetElementType() << "\n"
+           << "in term : " << n;
+        throw TypeCheckingExceptionPrivate(n, ss.str());
       }
     }
     return nodeManager->booleanType();