From d4699b181d643aeadd11b70729580ca1fab34ee3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Mar 2020 12:49:44 -0700 Subject: [PATCH] fix assertion Signed-off-by: Nikolaj Bjorner --- src/ast/macros/macro_manager.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index cb766e400..e732f4de3 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -341,7 +341,7 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, e for (;;) { macro_expander_rw proc(m, *this); proof_ref n_eq_r_pr(m); - SASSERT(m.get_fact(old_pr) == old_n); + SASSERT(!old_pr || m.get_fact(old_pr) == old_n); TRACE("macro_manager_bug", tout << "expand_macros:\n" << mk_pp(n, m) << "\n";); proc(old_n, r, n_eq_r_pr); new_pr = m.mk_modus_ponens(old_pr, n_eq_r_pr);