summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fmf
AgeCommit message (Expand)Author
2017-03-15Allow 0 argument recursive functions. Fixes bug 782.ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2017-02-07Generalize finite bound inference to unifiable variables in set membership li...ajreynol
2017-01-11Fix for when variables are (partially) bound in multiple ways, add regression...ajreynol
2017-01-04Marking regression test files as non-executable.Tim King
2016-12-07Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.ajreynol
2016-12-07Refactoring, generalization of bounded inference module. Simplification of re...ajreynol
2016-12-02Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --...ajreynol
2016-11-17Fix Makefiles in testAndres Notzli
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
2016-06-01Initial infrastructure for bounded set quantification (disabled). Refactoring...ajreynol
2016-05-23Fix related to parametric sorts whose interpretation is finite due to uninter...ajreynol
2016-04-11Minor fixes for inst match generators. Updates to qip.googleajreynol
2016-04-10More work on instantiation propagation. Enable external filtering of instanti...ajreynol
2016-03-07Minor change to F-Length inference in strings. No internal tracking of cardin...ajreynol
2016-02-23Fix term database for non-equal, congruent terms in master equality engine. D...ajreynol
2016-02-19Fixes and improvements for datatypes properties and splitting.ajreynol
2016-02-18Implement dynamic splitting for quantified formulas. Minor refactoring of re...ajreynol
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