summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2012-12-05Cleanup of arithmetic, and some new utility functions for the coming fcsimple...Tim King
2012-12-05This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ...Tim King
2012-12-04* Add support for --decision=justification + incremental (bug 437)Kshitij Bansal
2012-12-03Fix for fuzzer-found model bugClark Barrett
2012-12-01fix to TNode assertion (which is too strict, given lax ordering requirements ...Morgan Deters
2012-12-01Throw a logic exception if user makes an assertion using a STORE_ALLClark Barrett
2012-12-01remove instantiator frameworkMorgan Deters
2012-12-01Fix the way abstract values are typed; fixes some compliance issues.Morgan Deters
2012-12-01fix memory corruption issue in debug builds that led to unhelpful outputMorgan Deters
2012-12-01remove an obsolete (and incorrect) assertion in boolean-terms; also add faili...Morgan Deters
2012-12-01drastic simplification of quantifiers code regarding equality queries, instan...Andrew Reynolds
2012-12-01Fix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and Integer((...Tim King
2012-12-01Some fixes for boolean arraysMorgan Deters
2012-12-01fix #line annotation warningMorgan Deters
2012-12-01another part of last commitMorgan Deters
2012-12-01definition-expansion fixed for get-model, resolves bug 411Morgan Deters
2012-12-01Adding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA");...Tim King
2012-11-30Changing the documentation of ARR_TABLE_FUN to say (internal symbol).Tim King
2012-11-30Fix assertion in smt_engine's getValueClark Barrett
2012-11-30Updating the combination.cpp example.Tim King
2012-11-30renaming --smtlib to --smtlib-strict; removing --smtlib2 optionMorgan Deters
2012-11-30internal variables (skolems) aren't printed as part of the modelMorgan Deters
2012-11-30change detection/handling of output language more reasonably; fixes a nagging...Morgan Deters
2012-11-30quantifiers now uses master equality engine, preparation work to cleanup codeAndrew Reynolds
2012-11-30parametric datatypes fix related to non-ascribed type constructors introduced...Andrew Reynolds
2012-11-30Changes to SExpr to accept autoconversion from bool and const char*. Adding a...Tim King
2012-11-30Adding smtname level options for tlimit, rlimit, etc. Fix to the internal doc...Tim King
2012-11-30Partial fix for bug 435; still needs some effort.Morgan Deters
2012-11-30fix the syntax of assert-rewrite/-propagation/-reduction by putting the patte...François Bobot
2012-11-29reliable benchmark corresponding to bug468Kshitij Bansal
2012-11-29require type ascriptions for parametric datatype constructors (making them ca...Andrew Reynolds
2012-11-29fixes bug 438, incorporate subtypes into type unification when typechecking p...Andrew Reynolds
2012-11-29fix for andy: boolean terms stuff really shouldn't look at datatypes at all i...Morgan Deters
2012-11-29minor documentation fixMorgan Deters
2012-11-29Fix for nasty corner case found by fuzzer...Clark Barrett
2012-11-29Hack to support global variables for CVC language extended to export mechanism.Kshitij Bansal
2012-11-29Fixing function models with Boolean terms. Also, LAMBDA's should not be const.Clark Barrett
2012-11-28fix a potential race (have failed to reproduce)Kshitij Bansal
2012-11-28Fix for getValue. Now it can handle lambda applicationsClark Barrett
2012-11-28Attempted "quick-fix" for QF_UF performance regression since Boolean terms ad...Morgan Deters
2012-11-28treat all get commands like getValue (send only to lastWinner)Kshitij Bansal
2012-11-28Bug fix:Morgan Deters
2012-11-28fix: correct misleading comment in dump outputMorgan Deters
2012-11-27Functions and predicates over Boolean now work with --check-models and output...Morgan Deters
2012-11-27fix in CommandSequence invoke : maintain success/failure. Fixes bug 465.Kshitij Bansal
2012-11-27more mac fixesMorgan Deters
2012-11-27fix for some Mac buildsMorgan Deters
2012-11-27Simplify --help=decision with only currently supported optionsKshitij Bansal
2012-11-27do not turn on BV for QF_SATMorgan Deters
2012-11-27First chunk of boolean-terms support.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback