From 3c0e8cb182204504b371d4125a32756bf1c55610 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Apr 2019 11:42:55 -0700 Subject: [PATCH] fix model generation for tc/po Signed-off-by: Nikolaj Bjorner --- src/model/model.cpp | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/model/model.cpp b/src/model/model.cpp index 15344b35d..756fe2251 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -432,12 +432,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) } #endif else { - if (m.is_ite(f)) { - new_t = m.mk_app(f, args.size(), args.c_ptr()); - } - else { - new_t = ts.m_rewrite.mk_app(f, args.size(), args.c_ptr()); - } + new_t = ts.m_rewrite.mk_app(f, args.size(), args.c_ptr()); } if (t != new_t.get()) trail.push_back(new_t);