Age | Commit message (Collapse) | Author |
|
|
|
(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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* getModelValue to valuation
* getModelValue to theory engine
* getModelValue to theory
implemented getModelValue in bitvector
the purpose of getModelValue is to ask for a concrete value of a shared term
|
|
|
|
|
|
|
|
completeness
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|