summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-04-27Merge branch 'master' of https://github.com/CVC4/CVC4Clark Barrett
2015-04-27Fixed problem with private/public header clashClark Barrett
2015-04-27Disambiguate namespaces in options, fix permissionsClark Barrett
2015-04-27Updating failing unit tests.Tim King
2015-04-26Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullMode...ajreynol
2015-04-24More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fm...ajreynol
2015-04-24Fix sygus parser for non-tokenized operators, reenable regression. Fix for --...ajreynol
2015-04-24Fix compiler errors due to unbalanced throw specifiers.Clark Barrett
2015-04-23Merge branch 'master' into googleClark Barrett
2015-04-23Whitespace differenceClark Barrett
2015-04-23A few more minor updates to match google repository with CVC4 repositoryClark Barrett
2015-04-23Added option for --check-unsat-cores and various core bug fixes (merge of Mor...Liana Hadarean
2015-04-22Merge pull request #73 from kbansal/parser-dont-tokenizeKshitij Bansal
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-04-21Fix file permissionsClark Barrett
2015-04-21Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.ajreynol
2015-04-21Adding an example of a tester in SMT2.Tim King
2015-04-18Farkas proof coefficients.Tim King
2015-04-17Patch for Kshitij's fix on requriePhaseTianyi Liang
2015-04-17Merge pull request #72 from kbansal/decision-requirephaseKshitij Bansal
2015-04-17moved Minisat namespace into CVC4Finn Haedicke
2015-04-16Fix option --quant-fun-wd. Add mk_starexec script to contrib.ajreynol
2015-04-16Handle (degenerate) case of synthesis conjectures for constants. Disable del...ajreynol
2015-04-16disable failing sygus testsKshitij Bansal
2015-04-16update commentKshitij Bansal
2015-04-15string parser builtinop changesKshitij Bansal
2015-04-15bv parserchanges cleanupKshitij Bansal
2015-04-15fp builtinop parser changesKshitij Bansal
2015-04-15fp reorder tokens to match other occurencesKshitij Bansal
2015-04-15THEORY_INTS parser changesKshitij Bansal
2015-04-15THEORY_REAL_INTS parser changesKshitij Bansal
2015-04-15array theory builtinopKshitij Bansal
2015-04-15cleanupKshitij Bansal
2015-04-15dont tokenize bv operators (normal ones)Kshitij Bansal
2015-04-15Enabling the regression test: test/regress/regress0/unconstrained/mult1.smt2Tim King
2015-04-15Fix for unconstrained bug.Clark Barrett
2015-04-15Adding an example that violates an assertion during unconstrained simplificat...Tim King
2015-04-13Making CVC4::theory::quantifiers::PrenexQuantMode public for now.Tim King
2015-04-09disable string reqressions timing out after changeKshitij Bansal
2015-04-09DE requests respect requirePhaseKshitij Bansal
2015-04-09Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, an...ajreynol
2015-04-09Fix performance issue with variable triggers + instantiation restrictions.ajreynol
2015-04-09Bug fix negative contains cache.ajreynol
2015-04-08Make fun-def quantifiers carry the function app they define, make fun-def uti...ajreynol
2015-04-07Removing the reference to THEORY_BOOL from the equality engine. This theoryDejan Jovanovic
2015-04-07Minor fixes for cegqi.ajreynol
2015-04-02Merge pull request #71 from kbansal/const-are-triggersKshitij Bansal
2015-04-01Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun...ajreynol
2015-03-31fix no return value warningKshitij Bansal
2015-03-31fix echo command in --tear-down-incrementalKshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback