dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4
GNU General Public License v3.0
48 stars 36 forks source link

--slack-level 3 failures #258

Closed soonhokong closed 8 years ago

soonhokong commented 8 years ago
1568 - regression_nra_slack_level_3_17.smt2 (Failed)
1580 - regression_nra_slack_level_3_disjunct.smt2 (Failed)
1586 - regression_nra_slack_level_3_ea_beales.smt2 (Failed)
1610 - regression_nra_slack_level_3_fedor_12.smt2 (Failed)
1611 - regression_nra_slack_level_3_fedor_13.smt2 (Failed)
1612 - regression_nra_slack_level_3_fedor_14.smt2 (Failed)
1616 - regression_nra_slack_level_3_hansen_simple.smt2 (Failed)
1629 - regression_nra_slack_level_3_ml.smt2 (Failed)
1635 - regression_nra_slack_level_3_osmosis-backoff.smt2 (Failed)
1636 - regression_nra_slack_level_3_osmosis-bounce-ML5.smt2 (Failed)
1637 - regression_nra_slack_level_3_osmosis-bounce-ML6.smt2 (Failed)
1638 - regression_nra_slack_level_3_osmosis-bounce-ML7.smt2 (Failed)
1639 - regression_nra_slack_level_3_osmosis-bounce-ML8.smt2 (Failed)
1640 - regression_nra_slack_level_3_osmosis-hockey-ML2-d10.smt2 (Failed)
1641 - regression_nra_slack_level_3_osmosis-hockey-ML2.smt2 (Failed)
1642 - regression_nra_slack_level_3_osmosis-hockey-ML3-d10.smt2 (Failed)
1643 - regression_nra_slack_level_3_osmosis-hockey-ML3.smt2 (Failed)
1644 - regression_nra_slack_level_3_osmosis-hockey-ML4-d10.smt2 (Failed)
1645 - regression_nra_slack_level_3_osmosis-hockey-ML4.smt2 (Failed)
1646 - regression_nra_slack_level_3_osmosis-hockey-ML5-d10.smt2 (Failed)
1647 - regression_nra_slack_level_3_osmosis-hockey-ML5.smt2 (Failed)
1649 - regression_nra_slack_level_3_osmosis-simple.smt2 (Failed)
1667 - regression_nra_slack_level_3_tai_sin_03.smt2 (Failed)
1677 - regression_nra_slack_level_3_zenna_04.smt2 (Failed)
1680 - regression_nra_slack_level_3_zenna_09.smt2 (Failed)
scungao commented 8 years ago

Yeah I don't think level 3 will be useful; this should be easy to fix but I'll put it on low priority. Level 1 separates top level linear/nonlinear and should be all we need. Level 2 is introducing too many variables already and should only be useful on special benchmarks.

soonhokong commented 8 years ago

I'll do the following and close this issue:

scungao commented 8 years ago

Great, thanks.