diff options
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 748ac3f9d..7a4bf721f 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -41,9 +41,15 @@ public: TNode::iterator argument_it = n.begin(); TNode::iterator argument_it_end = n.end(); TypeNode::iterator argument_type_it = fType.begin(); - for(; argument_it != argument_it_end; ++argument_it) { + for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) { if((*argument_it).getType() != *argument_type_it) { - throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + std::stringstream ss; + ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)) + << "argument types do not match the function type:\n" + << "argument: " << *argument_it << "\n" + << "has type: " << (*argument_it).getType() << "\n" + << "not equal: " << *argument_type_it; + throw TypeCheckingExceptionPrivate(n, ss.str()); } } } |