diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-11 18:33:25 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-11 18:33:25 -0500 |
| commit | 67c730c76969d016b23b0c90b190be28fda9ac3f (patch) | |
| tree | f4a7279f7d4d0bdcd92268dc0f4111ef5676150c /src/smt/smt_engine.cpp | |
| parent | 98178c539c4eb502d3f3c3c4f1fcf0600d229b46 (diff) | |
Do not enable some SMT-COMP specific options by default (#4038)
Moves SMT-COMP-specific options to the SMT-COMP script. Both of these options have led to issues (segfaults or infinite loops).
Issue #789 can be downgraded to "minor" after this PR.
Btw, I did not add these specialized options to the "incremental" script of SMT-COMP, since I'm assuming they should not be used there.
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 27d06e104..fbc5821ce 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1627,35 +1627,6 @@ void SmtEngine::setDefaults() { Theory::setUninterpretedSortOwner(THEORY_UF); } - // Turn on ite simplification for QF_LIA and QF_AUFBV - // WARNING: These checks match much more than just QF_AUFBV and - // QF_LIA logics. --K [2014/10/15] - if(! options::doITESimp.wasSetByUser()) { - bool qf_aufbv = !d_logic.isQuantified() && - d_logic.isTheoryEnabled(THEORY_ARRAYS) && - d_logic.isTheoryEnabled(THEORY_UF) && - d_logic.isTheoryEnabled(THEORY_BV); - bool qf_lia = !d_logic.isQuantified() && - d_logic.isPure(THEORY_ARITH) && - d_logic.isLinear() && - !d_logic.isDifferenceLogic() && - !d_logic.areRealsUsed(); - - bool iteSimp = (qf_aufbv || qf_lia); - Trace("smt") << "setting ite simplification to " << iteSimp << endl; - options::doITESimp.set(iteSimp); - } - if(! options::compressItes.wasSetByUser() ){ - bool qf_lia = !d_logic.isQuantified() && - d_logic.isPure(THEORY_ARITH) && - d_logic.isLinear() && - !d_logic.isDifferenceLogic() && - !d_logic.areRealsUsed(); - - bool compressIte = qf_lia; - Trace("smt") << "setting ite compression to " << compressIte << endl; - options::compressItes.set(compressIte); - } if(! options::simplifyWithCareEnabled.wasSetByUser() ){ bool qf_aufbv = !d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_ARRAYS) && |