mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

flat only

Browse source 
remove option for uzers (users who are in reality fuzzers) to toggle flat option. The legacy arithmetic solver bakes in assumptions about flat format so it isn't helpful to expose this to fuzzers, I mean uzers.
This commit is contained in:
Nikolaj Bjorner 2022-06-30 19:59:46 -07:00
parent b618537322
commit ea2a843325
2 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -78,7 +78,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
void updt_local_params(params_ref const & _p) {
rewriter_params p(_p);
m_flat = p.flat();
m_flat = true;
m_max_memory = megabytes_to_bytes(p.max_memory());
m_max_steps = p.max_steps();
m_pull_cheap_ite = p.pull_cheap_ite();

1
src/params/rewriter_params.pyg
View file

@ -3,7 +3,6 @@ def_module_params('rewriter',
export=True,
params=(max_memory_param(),
max_steps_param(),
("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"),
("push_ite_arith", BOOL, False, "push if-then-else over arithmetic terms."),
("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."),
("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."),