From 9922c766b960b79178596d2dff64b72b3e28bad7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Aug 2022 17:39:14 -0700 Subject: [PATCH] add extra information for type error message a recent opened and closed bug report was due to an error of taking bit-wise or between two bit-vectors of different size. The error message was not understood by the user. Adding a little extra generic information to see if it helps. --- src/ast/bv_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 5b28bcf5e..351d037cb 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -620,7 +620,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p for (unsigned i = 0; i < num_args; ++i) { if (args[i]->get_sort() != r->get_domain(i)) { std::ostringstream buffer; - buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m); + buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " has sort " << mk_pp(args[i]->get_sort(), m) << " it does does not match declaration " << mk_pp(r, m); m.raise_exception(buffer.str()); return nullptr; }