mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

fix build, fix #1322

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-24 13:20:19 -07:00
parent 6300a78b82
commit 31dfc0c610
2 changed files with 15 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/cmd_context/cmd_context.cpp
View file

@ -1053,7 +1053,6 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
func_decls fs; func_decls fs;
if (!m_func_decls.find(s, fs)) { if (!m_func_decls.find(s, fs)) {
if (num_args == 0) { if (num_args == 0) {
//UNREACHABLE();
throw cmd_exception("unknown constant ", s); throw cmd_exception("unknown constant ", s);
} }
else else
@ -1065,7 +1064,6 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) to disumbiguate ", s); throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) to disumbiguate ", s);
func_decl * f = fs.first(); func_decl * f = fs.first();
if (f == 0) { if (f == 0) {
//UNREACHABLE();
throw cmd_exception("unknown constant ", s); throw cmd_exception("unknown constant ", s);
} }
if (f->get_arity() != 0) if (f->get_arity() != 0)
@ -1075,8 +1073,20 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
else { else {
func_decl * f = fs.find(m(), num_args, args, range); func_decl * f = fs.find(m(), num_args, args, range);
if (f == 0) { if (f == 0) {
//UNREACHABLE(); std::ostringstream buffer;
throw cmd_exception("unknown constant ", s); buffer << "unknown constant " << s << " ";
buffer << " (";
bool first = true;
for (unsigned i = 0; i < num_args; ++i, first = false) {
if (!first) buffer << " ";
buffer << mk_pp(m().get_sort(args[i]), m());
}
buffer << ") ";
if (range) buffer << mk_pp(range, m()) << " ";
for (unsigned i = 0; i < fs.get_num_entries(); ++i) {
buffer << "\ndeclared: " << mk_pp(fs.get_entry(i), m()) << " ";
}
throw cmd_exception(buffer.str().c_str());
} }
if (well_sorted_check_enabled()) if (well_sorted_check_enabled())
m().check_sort(f, num_args, args); m().check_sort(f, num_args, args);

2
src/util/container_util.h
View file

@ -31,7 +31,7 @@ Revision History:
template<class Set1, class Set2> template<class Set1, class Set2>
void set_intersection(Set1 & tgt, const Set2 & src) { void set_intersection(Set1 & tgt, const Set2 & src) {
svector<typename Set1::data> to_remove; svector<typename Set1::data> to_remove;
for (Set1::data itm : tgt) for (auto const& itm : tgt)
if (!src.contains(itm)) if (!src.contains(itm))
to_remove.push_back(itm); to_remove.push_back(itm);
while (!to_remove.empty()) { while (!to_remove.empty()) {