diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 73454b5258b..d3f6aca1421 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -820,10 +820,6 @@ def Function(name, *sig): def FreshFunction(*sig): """Create a new fresh Z3 uninterpreted function with the given sorts. - - >>> f = FreshFunction(IntSort(), IntSort()) - >>> f(f(0)) - f!0(f!0(0)) """ sig = _get_args(sig) if z3_debug(): diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index 7e3ef87ed48..02f4f6db4dd 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -126,7 +126,6 @@ bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_depen m_decl2macro_dep.insert(f, dep); TRACE("macro_insert", tout << "A macro was successfully created for: " << f->get_name() << "\n";); - SASSERT(false); // Nothing's forbidden anymore; if something's bad, we detected it earlier. // mark_forbidden(m->get_expr());