summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fmf
AgeCommit message (Expand)Author
2016-02-09Fix regression, minor change to output.ajreynol
2016-02-08Updates related to finite model finding and (co)datatypes. Bug fix enumerator...ajreynol
2016-02-01Simplify fmc model construction, add regression. Improve FMF debug assertions.ajreynol
2016-01-20Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant ...ajreynol
2016-01-19Bug fixes for model construction with codatatypes, add regressions.ajreynol
2016-01-18Bug fix rewriter for fun defs.ajreynol
2016-01-15Ensure model construction for parametric sorts involving uninterpreted sorts ...ajreynol
2015-12-22Always split on constructor types for datatypes involving uninterpreted sorts...ajreynol
2015-12-22Bug fix for cbqi, do not use model values for terms involving non-enumerable ...ajreynol
2015-11-06Changing file permissions to add or remove executable tag as appropriate.Tim King
2015-11-04Better combination of UF with cbqi, refactor quantifiers intialization.ajreynol
2015-06-27Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de...ajreynol
2015-04-27Disambiguate namespaces in options, fix permissionsClark Barrett
2015-04-26Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullMode...ajreynol
2015-04-23Merge branch 'master' into googleClark 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-21Fix file permissionsClark Barrett
2014-11-07Properly distinguish which EQC to assign values in datatypes, use assertRepre...ajreynol
2014-11-06Reenable regression. Add (for now, disabled) changes to datatypes theory com...ajreynol
2014-11-05More work on datatypes theory combination: fix bug in care graph, do not assi...ajreynol
2014-04-14Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ...Andrew Reynolds
2014-04-10Add support for cardinality constraints logic UFC. Add regressions in fmf/. ...Andrew Reynolds
2014-03-07Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodi...Morgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-11-11Change exit status to be more consistent with other command-line tools: 0 suc...Morgan Deters
2013-10-24Fix for bug515Clark Barrett
2013-09-18Support a personal build configuration and make rules.Morgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-09-09Another minor fix for datatypes to repair my previous commit.Andrew Reynolds
2013-05-22Add regressions for finite model findingAndrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback