| Age | Commit message (Expand) | Author |
|---|
| 2019-09-04 | Remove duplicate regression tests. (#3227) | Mathias Preiner |
| 2019-06-04 | Add check that result matches benchmark status (#3028) | Andres Noetzli |
| 2019-04-16 | Minor simplifications to theory quantifiers (#2953) | Andrew Reynolds |
| 2018-11-05 | Increasing coverage (#2683) | yoni206 |
| 2018-09-24 | Fix quantifiers selector over store rewrite (#2510) | Andrew Reynolds |
| 2018-09-22 | cmake: Added regression tests and target make regress. | Aina Niemetz |
| 2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz |
| 2018-09-06 | Refactor and document quantifiers variable elimination and conditional splitt... | Andrew Reynolds |
| 2018-09-04 | Make quantifiers strategies exit immediately when in conflict (#2099) | Andrew Reynolds |
| 2018-08-20 | Remove support for *.expect files in regressions (#2341) | Andres Noetzli |
| 2018-08-07 | Fix inference of pre and post conditions for non variable arguments. (#2237) | Andrew Reynolds |
| 2018-06-01 | Fix quantified bv variable elimination (#2039) | Andrew Reynolds |
| 2018-06-01 | Use monomial sum utility to solve for quantifiers macros (#2038) | Andrew Reynolds |
| 2018-05-22 | Set same options for proofs as for unsat cores (#1957) | Andres Noetzli |
| 2018-04-25 | Fix issue with multi-triggers that include variable triggers (#1810) | Andrew Reynolds |
| 2018-03-21 | Move regression tests to single Makefile.am (#1658) | Andres Noetzli |
| 2018-03-19 | Enable CEGQI for non-linear (#1674) | Andrew Reynolds |
| 2018-02-15 | Refactor regressions (#1581) | Andrew Reynolds |
| 2018-01-08 | Improvements to quant+BV/Bool variable elimination (#1495) | Andrew Reynolds |
| 2018-01-03 | Global negate (#1466) | Andrew Reynolds |
| 2017-12-20 | Fixes for cbqi-bv (#1449) | Andrew Reynolds |
| 2017-12-20 | Add explicit disequality handling when generating side condition for CBQI BV.... | Aina Niemetz |
| 2017-12-08 | Fixed side conditions for CBQI BV, added unit tests. (#1434) | Aina Niemetz |
| 2017-11-21 | Cegqi bv remove extract terms preprocess pass (#1376) | Andrew Reynolds |
| 2017-11-15 | Reenable some regressions, minor. (#1369) | Andrew Reynolds |
| 2017-11-14 | Clean Ceg Instantiators (#1365) | Andrew Reynolds |
| 2017-11-01 | CBQI BV choice expressions (#1296) | Andrew Reynolds |
| 2017-10-25 | CBQI BV: Add handling for missing operators. (#1274) | Aina Niemetz |
| 2017-10-23 | CBQI BV: Add ULT/SLT inverse handling. (#1268) | Aina Niemetz |
| 2017-10-13 | CBQI BV: Added EXTRACT handling. (#1240) | Aina Niemetz |
| 2017-10-12 | CBQI BV quick heuristics (#1239) | Andrew Reynolds |
| 2017-10-12 | Initial support for solving bit-vector inequalities (#1229) | Andrew Reynolds |
| 2017-10-11 | Enable regressions for CBQI BV and fix inverse for LSHR. (#1234) | Aina Niemetz |
| 2017-10-11 | Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224) | Mathias Preiner |
| 2017-10-11 | Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion ... | Andrew Reynolds |
| 2017-10-09 | CBQI BV: Add inverse for more operators. (#1213) | Aina Niemetz |
| 2017-09-29 | Simplify representation of inversion Skolems for bv cegqi (#1164) | Andrew Reynolds |
| 2017-09-29 | Initial working version of BV word-level instantiation (#1158) | Andrew Reynolds |
| 2017-09-14 | Remove unhandled subtypes (#1098) | Andrew Reynolds |
| 2017-08-04 | Set default language to smt lib 2.6 (including as a base language for sygus),... | ajreynol |
| 2017-06-30 | Minor change to trigger selection, fixes related to subtypes (in macros, cbqi... | ajreynol |
| 2017-06-15 | Add regression. | ajreynol |
| 2017-05-31 | Fix model construction for BV with cbqi. Minor change to defaults. | ajreynol |
| 2017-05-31 | Minor change to defaults, update smt comp script, minor changes to options in... | ajreynol |
| 2017-04-04 | Enable multi-trigger-linear by default, add option. | ajreynol |
| 2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole... | ajreynol |
| 2017-01-04 | Marking regression test files as non-executable. | Tim King |
| 2017-01-04 | Reverting two files encoding with DOS linebreaks back into using unix linebre... | Tim King |
| 2016-11-17 | Fix Makefiles in test | Andres Notzli |
| 2016-09-20 | More refactoring of cbqi. Add a few regressions. Add option for qcf. | ajreynol |
