summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-06-12More make submission stuffMorgan Deters
2014-06-12Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2014-06-12fixing bv inequality solver explanation buglianah
2014-06-12New application track script, new heuristics and all --tear-down-incremental....Morgan Deters
2014-06-12added bvcomp case to bv to bool liftinglianah
2014-06-11more fix-upsMorgan Deters
2014-06-11added optionException for trying to use abc in an non-abc buildlianah
2014-06-11more smtcomp-submission script workMorgan Deters
2014-06-11Flush output stream after result printed in portfolio.Morgan Deters
2014-06-11Fix for competition mode + parallel.Morgan Deters
2014-06-11Fix parallel run script.Morgan Deters
2014-06-11Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2014-06-11switched bv equality orderlianah
2014-06-12Update SMTCOMP script to handle all quantified logics.ajreynol
2014-06-11Fix an omission in bv sources.Morgan Deters
2014-06-11--best now implies --with-glpk --with-abcMorgan 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-11disable another test, after recent merges taking too longKshitij Bansal
2014-06-11disable failing testKshitij Bansal
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-10Add new --pb-rewrites options to QF_LIA run script for SMT-COMP.Morgan Deters
2014-06-10Some news about API changes.Morgan Deters
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-09Tim's options for QF_LIA and QF_LRA---SOI+approx.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-08test for prvs commit (tokenize emptyset)Kshitij 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-08sets translate: a different translation using axiomsKshitij Bansal
2014-06-06sets translator: fix for dagsKshitij Bansal
2014-06-06Merge pull request #28 from kbansal/setsKshitij Bansal
2014-06-06Fix submission script (again).Morgan Deters
2014-06-06rm warning from helloworld exampleKshitij 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback