Age | Commit message (Collapse) | Author |
|
* 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
|
|
|
|
|
|
|
|
finish removal of separateOutput
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Conflicts:
src/smt/boolean_terms.cpp
|
|
due to namesapce resolution std namespace was used instead, which hashes the string pointers leading to mayhem
|
|
|
|
export CXXFLAGS='-std=gnu++0x' before configure
fails all regressions in the parser
|
|
|
|
|