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, 3 insertions, 1 deletions

diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 5d97dda38..6f97a9662 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -46,12 +46,14 @@ class UfTypeRule {
         TypeNode currentArgument = (*argument_it).getType();
         TypeNode currentArgumentType = *argument_type_it;
         if (!currentArgument.isComparableTo(currentArgumentType)) {
+        //if (!currentArgument.isSubtypeOf(currentArgumentType)) {   //FIXME:typing
           std::stringstream ss;
           ss << "argument type is not a subtype of the function's argument "
              << "type:\n"
              << "argument:  " << *argument_it << "\n"
              << "has type:  " << (*argument_it).getType() << "\n"
-             << "not subtype: " << *argument_type_it;
+             << "not subtype: " << *argument_type_it << "\n"
+             << "in term : " << n;
           throw TypeCheckingExceptionPrivate(n, ss.str());
         }
       }