summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fmf
AgeCommit message (Expand)Author
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2017-11-03Suppport SAT logic (#1310)Andrew Reynolds
2017-09-28Improve finite model finding for recursive predicates (#1150)Andrew Reynolds
2017-09-10Ensure that expand definitions is called on all non-variable expressi… (#1070)Andrew Reynolds
2017-08-31Answer unknown when uf-ss=no-minimal is combined with cardinality constraints...Andrew Reynolds
2017-08-04Set default language to smt lib 2.6 (including as a base language for sygus),...ajreynol
2017-05-31Minor change to defaults, update smt comp script, minor changes to options in...ajreynol
2017-05-05Do not eliminate extended arithmetic symbols when finite model finding is on,...ajreynol
2017-04-28Do not eliminate non-standard arithmetic operators in recursive function defi...ajreynol
2017-04-24Fixes and simplifications for fmf mbqi.ajreynol
2017-04-14Fix for fmf-fun when the option is set by user command.ajreynol
2017-04-05Caching for fun def process, add regression.ajreynol
2017-03-22Minor fix for bounded integers.ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback