diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-20 11:19:50 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-20 11:19:50 +0000 |
commit | 2499bd64a5ac688573ebbcd6114983f64a8094eb (patch) | |
tree | 0d49608cf7c21298fbeb8606fa1943c96beb8652 /src/theory/uf | |
parent | 5a98094e8eee680d4f489e901107dfc484a1679f (diff) |
numerous bugfixes
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()); } } } |