remove assert, remove brittle pydoc example

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Feb 17, 2020 · 41ab578 · 41ab578
1 parent b6ee0b1
commit 41ab578
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 5 deletions.
diff --git 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
@@ -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());