From 41ab578593b5f3acf8d62b0fc3a3c7fa745ee67d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Feb 2020 00:35:47 -1000 Subject: [PATCH] remove assert, remove brittle pydoc example Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 4 ---- src/ast/macros/macro_manager.cpp | 1 - 2 files changed, 5 deletions(-) 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());