summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2014-06-11Fix for competition mode + parallel.Morgan Deters
2014-06-11switched bv equality orderlianah
2014-06-11Fix an omission in bv sources.Morgan Deters
2014-06-11Some clean-up, post bv-merge.Morgan Deters
2014-06-11Merge pull request #31 from kbansal/setsKshitij Bansal
2014-06-11fixed unit tests failureslianah
2014-06-11sets: comment out an assertion too strongKshitij Bansal
2014-06-11user/sat context issue in setsKshitij Bansal
2014-06-11fix in sets rewriterKshitij Bansal
2014-06-11fixing bv ackermanization cache buglianah
2014-06-10Merging Tim's pseudoboolean work from his fmcad14 branch.Tim King
2014-06-10reverting portfolio hacklianah
2014-06-10Merging CAV14 paper bit-vector work.lianah
2014-06-09Disallow copy/assignment of SmtEngine.Morgan Deters
2014-06-09Merge pull request #29 from kbansal/alternatefixKshitij Bansal
2014-06-09Add missing set of braces, fixes --trace.Morgan Deters
2014-06-08parseErrorHelper : factor out whole word matchingKshitij Bansal
2014-06-08Previous "repeat" fix required extra lookahead (leading to assert-fails). Fi...Morgan Deters
2014-06-08smt2 parser: tokenize emptyset only if theory enabledKshitij Bansal
2014-06-08Better error when there are \backslashes in |quoted symbols|.Morgan Deters
2014-06-08Allow 'repeat' as an SMT-LIB user symbol name (UFNIA/vcc-havoc does this).Morgan Deters
2014-06-06Merge pull request #28 from kbansal/setsKshitij Bansal
2014-06-06Patch for the subtype theoryof mode to make the equalities over disequal type...Tim King
2014-06-06sets: fix equality propagationKshitij Bansal
2014-06-06-{d,t} help => --show-{debug,trace}-tagsKshitij Bansal
2014-06-06option to hide stats which are zero (off by default), also some aliasesKshitij Bansal
2014-06-06Sets translate, and other short fixesKshitij Bansal
2014-06-05When printing in SMT, print N-ary bvadd/bvmul/concat/bvand/bvor/bvxor as binary.Morgan Deters
2014-06-04Add operator support (resolves bug #563).Morgan Deters
2014-06-04SmtEngine::checkModel() now checks that model values are of the correct type ...Morgan Deters
2014-06-04Fix usability issue with tear-down incremental mode.Morgan Deters
2014-06-04SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, bvor,...Morgan Deters
2014-06-03Support E-matching/QCF for Set operators.ajreynol
2014-06-01Fix for Windows builds (rlimit doesn't exist on Windows).Morgan Deters
2014-05-30Bug fix for string-opt2 (copied from Tianyi's branch).Morgan Deters
2014-05-30Improve --dt-stc-ind for multi-variable datatype properties.ajreynol
2014-05-30Fixes for --inst-max-levelajreynol
2014-05-28Minor changes to script. Disable cbqi sat.ajreynol
2014-05-28Add option to avoid dumping partial models/proofs.Andrew Reynolds
2014-05-27Some fixes to GC order in Java.Morgan Deters
2014-05-27New --tear-down-incremental mode, useful for debugging and performance profil...Morgan Deters
2014-05-27fix timespec printingKshitij Bansal
2014-05-27Revert "timespec printing bug"Kshitij Bansal
2014-05-27timespec printing bugKshitij Bansal
2014-05-27Fix typo in Java destruction code; should fix some recent bug reports of cras...Morgan Deters
2014-05-27Improved type-checking for tuple and record selects.Morgan Deters
2014-05-26Fix bug 567Kshitij Bansal
2014-05-26Fixing Tim's subtype/solving bug for arraysClark Barrett
2014-05-26Separating an implicit inclusion of smt_engine.h from theory.h.Tim King
2014-05-26Fixing a soundness bug due to the default implmentation of Theory::ppAssert()...Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback