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

remove more unsound rewrites #2575

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-23 02:56:31 -07:00
parent f3f233cf14
commit dee8a9f308
1 changed files with 2 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1828,14 +1828,8 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const*
result = m_util.re.mk_loop(args[0], f->get_parameter(1).get_int(), f->get_parameter(1).get_int());
return BR_REWRITE1;
}
// (loop (loop a lo hi) lo2) = (loop lo*lo2)
if (m_util.re.is_loop(args[0], a, lo, hi) && f->get_num_parameters() == 1) {
result = m_util.re.mk_loop(a, f->get_parameter(0).get_int() * lo);
return BR_REWRITE1;
}
// (loop (loop a lo) lo2 ..) = (loop lo*lo2)
if (m_util.re.is_loop(args[0], a, lo)) {
SASSERT(f->get_num_parameters() >= 1);
// (loop (loop a lo) lo2) = (loop lo*lo2)
if (m_util.re.is_loop(args[0], a, lo) && f->get_num_parameters() == 1) {
result = m_util.re.mk_loop(a, f->get_parameter(0).get_int() * lo);
return BR_REWRITE1;
}