mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix #6126

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-03 17:47:05 -07:00
parent d61d0f6a66
commit ac8aaed1d4
1 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ackermannization/ackr_model_converter.cpp
View file

@ -46,11 +46,15 @@ public:
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;
}