mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
cheap eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
94263167ec
commit
6c115bf896
|
@ -755,10 +755,10 @@ namespace smt {
|
|||
}
|
||||
|
||||
void setup::setup_lra_arith() {
|
||||
if (m_params.m_arith_mode == AS_OLD_ARITH)
|
||||
m_context.register_plugin(alloc(smt::theory_mi_arith, m_context));
|
||||
else
|
||||
m_context.register_plugin(alloc(smt::theory_lra, m_context));
|
||||
// if (m_params.m_arith_mode == AS_OLD_ARITH)
|
||||
// m_context.register_plugin(alloc(smt::theory_mi_arith, m_context));
|
||||
// else
|
||||
m_context.register_plugin(alloc(smt::theory_lra, m_context));
|
||||
}
|
||||
|
||||
void setup::setup_mi_arith() {
|
||||
|
|
Loading…
Reference in a new issue