From a9ebda105c0bfe94242c0cf702655411e78a662a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 1 Dec 2017 08:59:36 -0800 Subject: [PATCH] remove assertion that gets violated on exception path (declaration of datatypes are not getting removed) Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 3 +++ src/cmd_context/pdecl.cpp | 5 +++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 035d032bc..a6846eb4d 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1138,8 +1138,11 @@ static void parse_example() { decls.push_back(c.function("a", 0, 0, B)); expr a = c.parse_string("(assert a)", sorts, decls); std::cout << a << "\n"; + + expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))"); } + int main() { try { diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 7eac1f347..8a7359e3a 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -852,8 +852,7 @@ pdecl_manager::pdecl_manager(ast_manager & m): pdecl_manager::~pdecl_manager() { dec_ref(m_list); reset_sort_info(); - SASSERT(m_sort2psort.empty()); - SASSERT(m_table.empty()); + SASSERT(m_sort2psort.empty()); } psort * pdecl_manager::mk_psort_cnst(sort * s) { @@ -865,6 +864,8 @@ psort * pdecl_manager::mk_psort_cnst(sort * s) { return r; } +static unsigned r_count = 0; + psort * pdecl_manager::register_psort(psort * n) { TRACE("register_psort", tout << "registering psort...\n"; n->display(tout); tout << "\n";); psort * r = m_table.insert_if_not_there(n);