mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

support for smtlib2.6 datatype parsing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-04 21:15:44 -07:00
parent 5d17e28667
commit aac7773a52
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/cmd_context/cmd_context.cpp
View file

@ -795,7 +795,6 @@ void cmd_context::insert(symbol const & s, func_decl * f) {
dictionary<func_decls>::entry * e = m_func_decls.insert_if_not_there2(s, func_decls()); dictionary<func_decls>::entry * e = m_func_decls.insert_if_not_there2(s, func_decls());
func_decls & fs = e->get_data().m_value; func_decls & fs = e->get_data().m_value;
if (!fs.insert(m(), f)) { if (!fs.insert(m(), f)) {
UNREACHABLE();
std::string msg = "invalid declaration, "; std::string msg = "invalid declaration, ";
msg += f->get_arity() == 0 ? "constant" : "function"; msg += f->get_arity() == 0 ? "constant" : "function";
msg += " '"; msg += " '";