summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-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
2015-03-28printer change for string smtlib2Tianyi Liang
2015-03-25change const are triggers from false to true in equality enginesKshitij Bansal
2015-03-23Parsing support for define-fun-rec/define-funs-rec.ajreynol
2015-03-23Decouple counter-example guided quantifier instantiation from Sygus.ajreynol
2015-03-16Add requirePhase len(x) = 0.Tianyi Liang
2015-03-16Fixed proof unitialized memory and minor memory leaks.Liana Hadarean
2015-03-14Bug fix for BVTianyi Liang
2015-03-14Patches for 32-bit ARMTianyi Liang
2015-03-14Updating resize for occurence lists to properly resize the whole state.Dejan Jovanovic
2015-03-11Strings split on constant lengths, add length=0 to split lemma for empty string.ajreynol
2015-03-11Minor fixes and improvements to cegqi-si for linear arithmetic.ajreynol
2015-03-10CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf sig...ajreynol
2015-03-05Minor fixes. Extend cegqi-si to real arithmetic.ajreynol
2015-03-04More work on arithmetic single invocation synthesis conjectures.ajreynol
2015-02-27Revert "dummy commit to force nightly builds"Kshitij Bansal
2015-02-26Robust strategy for single invocation LIA synthesis conjectures. Add regress...ajreynol
2015-02-25Switch back to eager loop temporarily.Tianyi Liang
2015-02-24minor fix for internal string printTianyi Liang
2015-02-22New trigger options. --inst-no-entail on by default. Misc cleanup.ajreynol
2015-02-18dummy commit to force nightly buildsKshitij Bansal
2015-02-16Merge branch 'master' of https://github.com/CVC4/CVC4Kshitij Bansal
2015-02-16webget: curl follow redirectKshitij Bansal
2015-02-14Fix unit tests.ajreynol
2015-02-14attempt to fix win32 buildsKshitij Bansal
2015-02-13Minor cleanup, remove unused files.ajreynol
2015-02-13Handle recursive singleton case for codatatypes, add regression. Simplify im...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback