From ac8aaed1d4f409fa8b4fc60313fc5029fb18d731 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Jul 2022 17:47:05 -0700 Subject: [PATCH] fix #6126 --- src/ackermannization/ackr_model_converter.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index a5b2630c719..78fe6bef00a 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -46,11 +46,15 @@ class ackr_model_converter : public model_converter { void operator()(model_ref & md) override { TRACE("ackermannize", tout << (fixed_model? "fixed" : "nonfixed") << "\n";); - SASSERT(!fixed_model || md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions())); - model_ref& old_model = fixed_model ? abstr_model : md; - SASSERT(old_model.get()); - model * new_model = alloc(model, m); - convert(old_model.get(), new_model); + CTRACE("ackermannize", md, tout << *md << "\n"); + CTRACE("ackermannize", fixed_model, tout << *abstr_model << "\n"); + + model* new_model = alloc(model, m); + + if (abstr_model) + convert(abstr_model.get(), new_model); + if (md) + convert(md.get(), new_model); md = new_model; }