summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-11-12* Fix language bindings: various issuesMorgan Deters
2012-11-12minor bug fixes for quantifiers, added sort inference module (not ready to be...Andrew Reynolds
2012-11-11Fixes for the arithmetic normal form and rewriter to handle arbitrary constan...Tim King
2012-11-10Beautifying integer_cln_imp.hTim King
2012-11-10Fix to quantifier rewritting not being idempotent. See bug 441.Tim King
2012-11-10Removing rewriter call in SmtEngine::addFormula().Tim King
2012-11-10Fixed missing \ in uflra/Makefile.maClark Barrett
2012-11-10Fix for bug 439. Delta computation now includes disequality information.Tim King
2012-11-10Change run-regression script to *additionally* run a second test with --check...Morgan Deters
2012-11-10Updates to Clark's commit r4540:Morgan Deters
2012-11-10fix typo in language bindingsMorgan Deters
2012-11-10Finally tracked down problems in regressions and fuzz results (this alsoClark Barrett
2012-11-09TheoryEngineModelBuilder::buildModel() is only called once with fullModel=tru...Morgan Deters
2012-11-09export null nodes (fixes a bug in portfolio model stuff)Kshitij Bansal
2012-11-09Test that breaks arithmetic model building due to disequality terms.Tim King
2012-11-09Arithmetic problem that fails --check-models due incompleteness with multipli...Tim King
2012-11-09Bug-fix for a crash involving improperly-thrown exceptions; also, add LogicEx...Morgan Deters
2012-11-09In non-linear logics, rewrite DIVISION, INTS_DIVISION, and INTS_MODULUS into ...Morgan Deters
2012-11-09another DISTCLEANFILES entry, for proper "make distclean" behavior (fixes "di...Morgan Deters
2012-11-09Fix for another model assertion failureClark Barrett
2012-11-08Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases fo...Tim King
2012-11-08fix "make distcheck"Morgan Deters
2012-11-08Review of trunk r4525 (TypeNode::getBaseType()):Morgan Deters
2012-11-08Improved support for division by zero. This adds the *_TOTAL kinds and unint...Tim King
2012-11-08exception fixMorgan Deters
2012-11-08Fixed two small bugs in model generationClark Barrett
2012-11-08Added getBaseType - Morgan please checkClark Barrett
2012-11-08added support for parametric datatypes in smt2 parser, includes support for '...Andrew Reynolds
2012-11-07* Type ascription bug fixed (resolves bug 432), but there are others I discov...Morgan Deters
2012-11-07Fix to a bug in integer mod lemmas.Tim King
2012-11-06fix issue in compatibility layer that could segfaultMorgan Deters
2012-11-05Fix to the context dependent static learning code.Tim King
2012-11-05fixes for replacement function libraryMorgan Deters
2012-11-05fixes for mac osMorgan Deters
2012-11-05fix for tarball building (fixes debian and distcheck problems in nightly builds)Morgan Deters
2012-11-02more minor updates to inst gen and representative selection, clean up of equa...Andrew Reynolds
2012-10-31cleaning up some of the equality query stuff, implemented a new representativ...Andrew Reynolds
2012-10-30delta of a model-building failure caseDejan Jovanović
2012-10-29more updates and minor bug fixes for fmf/inst-gen quantifier instantiationAndrew Reynolds
2012-10-29Tweak to options configuration for turning off minisat elimination when model...Clark Barrett
2012-10-29Disable minisat elimination when models are onClark Barrett
2012-10-29Disable some array optimizations when models are onClark Barrett
2012-10-29auflia directory missing from regression summary - fixedClark Barrett
2012-10-26Fix to subrange type enumerator, and its unit test. Resolves bug 436.Morgan Deters
2012-10-26bug fix for parametric datatypes, previously datatypes theory/rewriter was no...Andrew Reynolds
2012-10-26Fix for bug 430. d_delta in PartialModel was never being computed. (Delta rem...Tim King
2012-10-26build options sources into distribution tarballs (in the same way that antlr ...Morgan Deters
2012-10-26new boost.m4 makes boost-thread require boost-system. relax this dependence ...Morgan Deters
2012-10-26better parametric datatype arity checking; fixes bug 433Morgan Deters
2012-10-26Fixed a failing datatype regression with check-modelsClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback