From 91045d3e4ae4f88f3eb4dbd4ee8e6197d15123ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Feb 2022 10:29:57 +0200 Subject: [PATCH] two words --- src/ast/rewriter/th_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index bb29b53db..3bc9c4ce1 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -305,12 +305,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg { expr * arg1 = ite->get_arg(1); expr * arg2 = ite->get_arg(2); - if (m().is_ite(arg1) && arg1->get_ref_count() == 1) // do not apply on shared terms, since it may blowup + if (m().is_ite(arg1) && arg1->get_ref_count() == 1) // do not apply on shared terms, since it may blow up todo.push_back(to_app(arg1)); else if (!m().is_value(arg1)) return false; - if (m().is_ite(arg2) && arg2->get_ref_count() == 1) // do not apply on shared terms, since it may blowup + if (m().is_ite(arg2) && arg2->get_ref_count() == 1) // do not apply on shared terms, since it may blow up todo.push_back(to_app(arg2)); else if (!m().is_value(arg2)) return false;