mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

remove assertion that gets violated on exception path (declaration of datatypes are not getting removed)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-01 08:59:36 -08:00
parent b96dacfff2
commit a9ebda105c
2 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
examples/c++/example.cpp
View file

@ -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 {

5
src/cmd_context/pdecl.cpp
View file

@ -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);