SRI-CSL / yices2 / 28736876360

71%

Build Type

push

github

Committed by web-flow

Commit Message

Re-enable bound strengthening and diophantine check in simplex (#651)

* Re-enable bound strengthening and diophantine check in simplex

Commit 14d675fc ('Test code', 2018) disabled these integer-feasibility
phases with 'if (false && ...)' guards, leaving only the integrality
check before branch & bound. This caused large slowdowns on easy
QF_LIA instances with mod/div (issue #410: 0.003s in 2.5.x vs 812s
in 2.6.4). Restore the four calls and add a regression test.

* Replace iss547 test instance

With the integer-feasibility phases re-enabled, the original instance
solves in under a second, so the 1s timeout it relies on never fires.
Use a Cornuejols-Dawande market-split instance instead, which is hard
for branch & bound.

Coverage Stats

4 of 4 new or added lines in 1 file covered. (100.0%)

15 existing lines in 2 files now uncovered.

95532 of 134190 relevant lines covered (71.19%)

1620969.82 hits per line