diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-13 00:12:02 -0500 |
|---|---|---|
| committer | Mathias Preiner <mathias.preiner@gmail.com> | 2017-10-12 22:12:02 -0700 |
| commit | 39a85cc99f3b9f3d203490f5918ebe56bd916d64 (patch) | |
| tree | 1962850621944d07af786ff491463e043aefcff1 /test/regress/regress0/quantifiers/anti-sk-simp.smt2 | |
| parent | 5031c6d9a08c84a6e8fe5019c6e278b8b2d7a238 (diff) | |
CBQI BV quick heuristics (#1239)
Adds two heuristics for cbqi-bv, both disabled by default.
The first optimistically solves for boundary points of inequalities.
The second randomly interleaves inversion and value instantiations.
Adds some newly solved regressions from SMT LIB.
Diffstat (limited to 'test/regress/regress0/quantifiers/anti-sk-simp.smt2')
0 files changed, 0 insertions, 0 deletions