Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
|
|
* the newVar interface of the sat solver now changed to include (isTheoryLiteral, preRegister, canEliminate)
* when bitblast-eager all bv atoms are (theory=false, prereg = true, canelim = true)
* bitblast-eager implies decision=internal
|
|
|
|
|
|
|
|
* update documentation
* update the cut-release script
* spelling/wording updates
* add a (previously-failing) fuzzer regression
|
|
|
|
|
|
|
|
|
|
long ago
|
|
add .mailmap
|
|
|
|
|
|
|
|
(ironic, yes, but model-based solver doesn't yet produce models)
|
|
|
|
|
|
|
|
* one that Tim found in model generation for records containing Booleans
* another that the fuzzer found in quantifiers + check-models
Test cases enabled/added for both.
|
|
|
|
|
|
|
|
|
|
* Comment cleanup
* Spelling fixes
* Fix warnings
* Documentation updates
* References in docs to cryptominisat removed
* Unneeded scope resolutions removed
* Old, unused regression removed
|
|
|
|
previously-failing testcase.
|
|
|
|
shared terms.
|
|
|
|
Minor changes to model-based array solver
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Minor fixes to bv and theory_engine
|
|
|
|
|
|
|
|
|