Age | Commit message (Expand) | Author |
2012-12-01 | drastic simplification of quantifiers code regarding equality queries, instan... | Andrew Reynolds |
2012-12-01 | Fix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and Integer((... | Tim King |
2012-12-01 | Some fixes for boolean arrays | Morgan Deters |
2012-12-01 | fix #line annotation warning | Morgan Deters |
2012-12-01 | another part of last commit | Morgan Deters |
2012-12-01 | definition-expansion fixed for get-model, resolves bug 411 | Morgan Deters |
2012-12-01 | Adding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA");... | Tim King |
2012-11-30 | Changing the documentation of ARR_TABLE_FUN to say (internal symbol). | Tim King |
2012-11-30 | Fix assertion in smt_engine's getValue | Clark Barrett |
2012-11-30 | Updating the combination.cpp example. | Tim King |
2012-11-30 | renaming --smtlib to --smtlib-strict; removing --smtlib2 option | Morgan Deters |
2012-11-30 | internal variables (skolems) aren't printed as part of the model | Morgan Deters |
2012-11-30 | change detection/handling of output language more reasonably; fixes a nagging... | Morgan Deters |
2012-11-30 | quantifiers now uses master equality engine, preparation work to cleanup code | Andrew Reynolds |
2012-11-30 | parametric datatypes fix related to non-ascribed type constructors introduced... | Andrew Reynolds |
2012-11-30 | Changes to SExpr to accept autoconversion from bool and const char*. Adding a... | Tim King |
2012-11-30 | Adding smtname level options for tlimit, rlimit, etc. Fix to the internal doc... | Tim King |
2012-11-30 | Partial fix for bug 435; still needs some effort. | Morgan Deters |
2012-11-30 | fix the syntax of assert-rewrite/-propagation/-reduction by putting the patte... | François Bobot |
2012-11-29 | reliable benchmark corresponding to bug468 | Kshitij Bansal |
2012-11-29 | require type ascriptions for parametric datatype constructors (making them ca... | Andrew Reynolds |
2012-11-29 | fixes bug 438, incorporate subtypes into type unification when typechecking p... | Andrew Reynolds |
2012-11-29 | fix for andy: boolean terms stuff really shouldn't look at datatypes at all i... | Morgan Deters |
2012-11-29 | minor documentation fix | Morgan Deters |
2012-11-29 | Fix for nasty corner case found by fuzzer... | Clark Barrett |
2012-11-29 | Hack to support global variables for CVC language extended to export mechanism. | Kshitij Bansal |
2012-11-29 | Fixing function models with Boolean terms. Also, LAMBDA's should not be const. | Clark Barrett |
2012-11-28 | fix a potential race (have failed to reproduce) | Kshitij Bansal |
2012-11-28 | Fix for getValue. Now it can handle lambda applications | Clark Barrett |
2012-11-28 | Attempted "quick-fix" for QF_UF performance regression since Boolean terms ad... | Morgan Deters |
2012-11-28 | treat all get commands like getValue (send only to lastWinner) | Kshitij Bansal |
2012-11-28 | Bug fix: | Morgan Deters |
2012-11-28 | fix: correct misleading comment in dump output | Morgan Deters |
2012-11-27 | Functions and predicates over Boolean now work with --check-models and output... | Morgan Deters |
2012-11-27 | fix in CommandSequence invoke : maintain success/failure. Fixes bug 465. | Kshitij Bansal |
2012-11-27 | more mac fixes | Morgan Deters |
2012-11-27 | fix for some Mac builds | Morgan Deters |
2012-11-27 | Simplify --help=decision with only currently supported options | Kshitij Bansal |
2012-11-27 | do not turn on BV for QF_SAT | Morgan Deters |
2012-11-27 | First chunk of boolean-terms support. | Morgan Deters |
2012-11-27 | Tuples and records merge. Resolves bug 270. | Morgan Deters |
2012-11-26 | Improved implementation of Integer::length() with CLN enabled. Additional te... | Tim King |
2012-11-26 | rolling back r4625 for now (closes bug 464), Andy we should talk about this a... | Morgan Deters |
2012-11-26 | fixup for incremental solving | Dejan Jovanović |
2012-11-26 | Removing DioSolver::acceptableOriginalNodes(). This assertion was too strong,... | Tim King |
2012-11-26 | Adding support for a master equality engine. Each theory gets the master equa... | Dejan Jovanović |
2012-11-26 | Improving arithmetic debugging output. | Tim King |
2012-11-26 | don't include internal variables in model output | Morgan Deters |
2012-11-26 | some fixes to language bindings and function visibility | Morgan Deters |
2012-11-25 | This commit fixes two incompleteness bugs (461, 459) introduced in r4611 dues... | Tim King |