mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

add extra information for type error message

Browse source 
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.
This commit is contained in:
Nikolaj Bjorner 2022-08-28 17:39:14 -07:00
parent dd91fab6f4
commit 9922c766b9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/bv_decl_plugin.cpp
View file

@ -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;
}