diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-30 09:02:51 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-30 09:03:20 -0500 |
commit | 303b91f3f5b8df1a884566a7d433ced17f0cd352 (patch) | |
tree | ebe6334ca8a415a4d5a24a83ee40441419c93876 /src/theory/uf | |
parent | ae1d4e4f05fdc2db61d7de7efee5bd567363ceef (diff) |
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.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 4 |
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()); } } |