summaryrefslogtreecommitdiff
path: root/test/unit
AgeCommit message (Expand)Author
2011-03-10Fix bug 246 (occasional buffer overflow related to varargs in assertion-failu...Morgan Deters
2011-02-28Review of statistics code. Added lots of documentation, and fixed an issue (...Morgan Deters
2011-02-26Merge from theory-break-dependences branch to break Theory and TheoryEngine d...Morgan Deters
2011-01-05fix for build errorsDejan Jovanović
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-12-14congruence closure module now supports things other than APPLY_UF; ported fro...Morgan Deters
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-11-17fix improper CongruenceClosureWhite test by merging from a uf branch; fixes t...Morgan Deters
2010-11-16Added Theory::presolve().Tim King
2010-11-15Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printerMorgan Deters
2010-11-15This commit merges the arith-prop-opt branch into the main trunk. This was do...Tim King
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-10-27fix test MakefileMorgan Deters
2010-10-26Cleaning up some header filesChristopher L. Conway
2010-10-24Adding unit test for InteractiveShellChristopher L. Conway
2010-10-22Merging main/getopt.cpp, main/usage.h, and smt/options.h inChristopher L. Conway
2010-10-21* Option --no-type-checking now disables type checks in SmtEngineChristopher L. Conway
2010-10-20fix bug #220 (assertion fails if no query/check-sat); add bug220.smt2 and bug...Morgan Deters
2010-10-12minor unit test fix-upsMorgan Deters
2010-10-12hooked up "we are incomplete" flag after conversation with Tim (a theory noti...Morgan Deters
2010-10-12Merge from cc-memout branch. Here are the main pointsMorgan Deters
2010-10-10additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp...Morgan Deters
2010-10-09reverting some changes to parser from last commitMorgan Deters
2010-10-09fix to unit testsMorgan Deters
2010-10-08* (define-fun...) now has proper type checking in non-debug buildsMorgan Deters
2010-10-07NodeSelfIterator implementation and unit test (resolves bug #204); also fix P...Morgan Deters
2010-10-03file header documentation regenerated with contributors names; no code modifi...Morgan Deters
2010-10-01re-add no-deprecated to C sources; update some file-level documentation; firs...Morgan Deters
2010-10-01replacement implementation for clock_gettime() on mac os x, build portability...Morgan Deters
2010-09-30fixed a number of problems with mac os x builds. build now works on mac os x...Morgan Deters
2010-09-28fix pre-registration of operator, previously committed; clean up theory engin...Morgan Deters
2010-09-28fix unit test for kinded iterators in Node/TNodeMorgan Deters
2010-09-27- This update adds DynamicArray<T>. This is a bare bones heap allocated arra...Tim King
2010-09-22Fixing NodeBuilderBlackChristopher L. Conway
2010-09-21some code cleanup, documentation, review of "kinded-iterator" code, and addit...Morgan Deters
2010-09-13make Node iterators more STL-friendly, resolves bug #196Morgan Deters
2010-09-13* New normal form for arithmetic is in place.Tim King
2010-09-02"Leftist NodeBuilders" are now supported.Morgan Deters
2010-09-02* add TimerStat statistic typeMorgan Deters
2010-08-17Merge from "cc" branch:Morgan Deters
2010-08-17Add "no trash" CDMap elements, so that CDMap elements can themselvesMorgan Deters
2010-08-16Fixing failures in minisatDejan Jovanović
2010-07-29fix TheoryEngineWhite, add documentation; related to bug #188Morgan Deters
2010-07-28Forcing a type check on Node construction in debug mode (Fixes: #188)Christopher L. Conway
2010-07-28fixed theory engine white test for new (old) theoryOf() behavior (re: bug 188)Morgan Deters
2010-07-27Adding optional 'check' parameter to getType() methodsChristopher L. Conway
2010-07-22incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool);...Morgan Deters
2010-07-08context work to support cdmaps with elements allocated in context memoryMorgan Deters
2010-07-07Shared term manager tested and workingClark Barrett
2010-07-07Added shared term manager. Basic mechanism for identifying shared terms isClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback