mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 19:21:22 +00:00
Code Activity

two words

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-02-20 10:29:57 +02:00
parent 9a1a72867c
commit 91045d3e4a
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/th_rewriter.cpp
View file

@ -305,12 +305,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
expr * arg1 = ite->get_arg(1); expr * arg1 = ite->get_arg(1);
expr * arg2 = ite->get_arg(2); 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)); todo.push_back(to_app(arg1));
else if (!m().is_value(arg1)) else if (!m().is_value(arg1))
return false; 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)); todo.push_back(to_app(arg2));
else if (!m().is_value(arg2)) else if (!m().is_value(arg2))
return false; return false;