mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

force flat for solver 2, fix #4789

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-12 13:01:38 -08:00
parent 5d10cb7af4
commit d61f30fdc6
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/asserted_formulas.cpp
View file

@ -141,6 +141,8 @@ void asserted_formulas::set_eliminate_and(bool flag) {
// seq theory solver keeps terms in normal form and has to interact with side-effect of rewriting
m_params.set_bool("coalesce_chars", m_smt_params.m_string_solver != symbol("seq"));
m_params.set_bool("som", true);
if (m_smt_params.m_arith_mode == arith_solver_id::AS_OLD_ARITH)
m_params.set_bool("flat", true);
m_rewriter.updt_params(m_params);
flush_cache();
}