projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
add bag.fold operator (#7718)
[cvc5.git] / test / regress / regress2 /
2021-11-08 Aina Niemetzsets: Rename kinds with a more consistent naming scheme... tree | commitdiff
2021-10-28 Abdalrhman MohamedFix `(set-info <sexpr>)` parsing and printing bugs... tree | commitdiff
2021-10-25 Andrew ReynoldsAdd new method for enumerating unsat queries with SyGuS... tree | commitdiff
2021-10-07 Andrew ReynoldsMake the cardinality of the alphabet of strings configu... tree | commitdiff
2021-09-22 Mathias PreinerRemove CVC language support (#7219) tree | commitdiff
2021-09-21 Andres NoetzliFix handling of conversions between FP and reals (... tree | commitdiff
2021-09-01 Haniel Barbosa[proof] [sat] Fix lost reference to reason when process... tree | commitdiff
2021-09-01 Andrew ReynoldsFix issues with cyclic proofs due to double SYMM applic... tree | commitdiff
2021-08-26 Gereon KremerImprove integration of nonlinear arithmetic into the... tree | commitdiff
2021-08-02 Mathias Preinerbv: Enable equality engine for bitblast-internal. ... tree | commitdiff
2021-07-29 Haniel Barbosa[proofs] Set BV solver to better proof-producing one... tree | commitdiff
2021-07-29 Andrew ReynoldsIntegrate central equality engine approach into theory... tree | commitdiff
2021-07-27 Andres NoetzliAdd regression for fixed `str.indexof_re` issue (#6938) tree | commitdiff
2021-07-01 Andrew ReynoldsAdd recursive function definitions to subsolver in... tree | commitdiff
2021-06-16 Aina NiemetzMake symfpu a required dependency. (#6749) tree | commitdiff
2021-06-11 Haniel BarbosaBetter support for HOL parsing and set up (#6697) tree | commitdiff
2021-06-10 Andrew ReynoldsEnsure bv2nat and int2bv are not rewritten when using... tree | commitdiff
2021-06-04 Andres NoetzliFix handling of start index in `str.indexof_re` (#6674) tree | commitdiff
2021-06-03 yoni206Renaming pow2 to p2 in regression tests (#6675) tree | commitdiff
2021-06-02 Aina NiemetzRemove redundant logic ALL_SUPPORTED. (#6664) tree | commitdiff
2021-05-28 Andres NoetzliDisable `--jh-rlv-order` for slow regressions (#6633) tree | commitdiff
2021-05-27 Andres NoetzliFix `str.replace_re` and `str.replace_re_all` (#6615) tree | commitdiff
2021-05-27 Andrew ReynoldsEnable new justification heuristic by default (#6613) tree | commitdiff
2021-05-21 Andrew ReynoldsFix tests of unsat cores (#6593) tree | commitdiff
2021-05-19 Haniel BarbosaChange the default unsat cores (#6571) tree | commitdiff
2021-05-18 Andres NoetzliFix `collectEmptyEqs()` in string utils (#6562) tree | commitdiff
2021-05-17 Gereon KremerImprove integration of CAD with nl-Ext (#6542) tree | commitdiff
2021-05-07 Aina NiemetzMove slow regressions and update guidelines. (#6508) tree | commitdiff
2021-05-06 Andrew ReynoldsDiscard duplicate terms in patterns (#6501) tree | commitdiff
2021-04-27 Andrew ReynoldsMove slow regression to regress3 (#6451) tree | commitdiff
2021-04-25 Andrew ReynoldsMore check models (#6439) tree | commitdiff
2021-04-24 Andrew ReynoldsImprove getValue for non-evaluated operators (#6436) tree | commitdiff
2021-04-22 Andrew ReynoldsFix models for sygus-inference, bv2int, real2int (... tree | commitdiff
2021-04-22 Haniel BarbosaReconciling proofs and unsat cores (#6405) tree | commitdiff
2021-03-16 Haniel Barbosa[proof-new] Renaming proof option to be in sync with... tree | commitdiff
2021-03-16 Haniel Barbosa[proof-new] Disabling proofs on regressions with known... tree | commitdiff
2021-03-06 Mathias PreinerRemove SMT-LIB 2.5 and 2.0 support. (#6068) tree | commitdiff
2021-01-20 Aina NiemetzSMT2 parser: Do not add non-linear symbols for linear... tree | commitdiff
2020-12-17 Andrew ReynoldsSimplify and fix check models (#5685) tree | commitdiff
2020-12-10 Andrew ReynoldsRefactor regressions (#5639) tree | commitdiff
2020-12-08 Gereon KremerAdd regression from #1978. (#5552) tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... tree | commitdiff
2020-12-02 Gereon KremerAdd regressions from #3687. (#5553) tree | commitdiff
2020-12-01 Gereon KremerAdd regressions for #4707. (#5555) tree | commitdiff
2020-11-23 Andrew ReynoldsChange UF ho to ppRewrite instead of expand definition... tree | commitdiff
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on... tree | commitdiff
2020-11-09 Andrew ReynoldsDo not regress explanations of datatype lemmas (#5376) tree | commitdiff
2020-10-14 yoni206bv2int: implementing the iand-sum mode (#5265) tree | commitdiff
2020-10-14 yoni206bv2int: rewritings and unsat cores (#5263) tree | commitdiff
2020-10-06 yoni206bv-to-int: change order of passes (#5208) tree | commitdiff
2020-09-23 yoni206bv2int: new options for bvand translation (#5096) tree | commitdiff
2020-09-16 yoni206bv2int: support models in tests (#5068) tree | commitdiff
2020-09-10 yoni206bv2int: improvement in lazy failures (#5020) tree | commitdiff
2020-09-03 yoni206Changing the handled operators in bv2int preprocessing... tree | commitdiff
2020-08-28 yoni206Incremental support for bv_to_int (#4967) tree | commitdiff
2020-08-24 Mathias PreinerIncrease regress level to 2 for production build. ... tree | commitdiff
2020-08-19 Andres Noetzli[Regressions] Do not test `--check-proofs` anymore... tree | commitdiff
2020-07-13 Andrew ReynoldsAdd support for string/sequence update (#4725) tree | commitdiff
2020-07-11 yoni206Changing bv_to_int options (#4721) tree | commitdiff
2020-07-09 Andrew ReynoldsDisable unsat cores in timeout regression (#4713) tree | commitdiff
2020-06-10 Andres NoetzliAdd support for str.replace_re/str.replace_re_all ... tree | commitdiff
2020-05-23 Andrew ReynoldsRefactor operator elimination in arithmetic (#4519) tree | commitdiff
2020-05-19 Andres NoetzliMake SolveEq and PlusCombineLikeTerms idempotent (... tree | commitdiff
2020-05-02 Andrew ReynoldsMove slow regression to regress3 (#4430) tree | commitdiff
2020-04-28 Andrew ReynoldsSupport the SMT-LIB Unicode string standard by default... tree | commitdiff
2020-04-28 Andrew ReynoldsUpdate cardinality in strings to unicode standard ... tree | commitdiff
2020-04-22 Abdalrhman MohamedConvert V2.5 SMT regressions to V2.6. (#4319) tree | commitdiff
2020-04-21 Andrew ReynoldsMake option names related to CEGQI consistent (#4316) tree | commitdiff
2020-04-19 Andrew ReynoldsDisable unsat cores on nec regression (#4330) tree | commitdiff
2020-04-17 Mathias PreinerSyGuS instantiation quantifiers module (#3910) tree | commitdiff
2020-04-12 Andrew ReynoldsMove slow nl regression to regress3 (#4276) tree | commitdiff
2020-04-01 Aina NiemetzRename checkValid/query to checkEntailed. (#4191) tree | commitdiff
2020-03-31 Andrew ReynoldsFixing regressions (#4189) tree | commitdiff
2020-03-30 Andrew ReynoldsSupport indexed operators re.loop and re.^ (#4167) tree | commitdiff
2020-03-22 Abdalrhman MohamedConvert V1 Sygus files to V2. (#4136) tree | commitdiff
2020-03-19 yoni206Bv2int fail on demand tree | commitdiff
2020-03-12 Andrew ReynoldsAdd options for nec regression (#4056) tree | commitdiff
2020-03-11 Andrew ReynoldsSwitch to Nodes for conjecture generator (#4026) tree | commitdiff
2020-03-06 Andrew ReynoldsRemove tester name from APIs (#3929) tree | commitdiff
2020-03-06 Andrew ReynoldsSupport default sygus grammar construction for sets... tree | commitdiff
2020-02-25 yoni206bv_to_int preprocessing pass tree | commitdiff
2020-02-03 Andrew ReynoldsExample inference utility (#3670) tree | commitdiff
2020-01-14 Andres NoetzliDisable unsat cores for regression that times out ... tree | commitdiff
2020-01-07 Andrew ReynoldsUpdate any-constant and normalization policies for... tree | commitdiff
2019-12-12 Andrew ReynoldsMake CEGIS sampling robust to non-vanilla CEGIS (#3559) tree | commitdiff
2019-12-05 Andrew ReynoldsRefactor mode options for Unif+PI (#3531) tree | commitdiff
2019-09-19 Andrew ReynoldsSupport context-(in)dependent decision strategies.... tree | commitdiff
2019-09-18 Andrew ReynoldsDecouple fmf-bound and finite-model-find (#3297) tree | commitdiff
2019-09-06 Mathias PreinerRemove SMT1 parser. (#3228) tree | commitdiff
2019-09-04 Mathias PreinerRemove duplicate regression tests. (#3227) tree | commitdiff
2019-08-30 Andres NoetzliBetter heuristic for str.code/re.range (#3220) tree | commitdiff
2019-08-22 Andrew Reynolds Local substitutions for context-depdendent simplificat... tree | commitdiff
2019-08-02 Andrew ReynoldsSupport default sygus grammar for strings (#3148) tree | commitdiff
2019-07-31 Haniel BarbosaParsing THF and adding several regressions (#3131) tree | commitdiff
2019-06-10 Andrew ReynoldsOptimization for negative concatenation membership... tree | commitdiff
2019-06-04 Andres NoetzliEnable proof checking for QF_LRA benchmarks (#2928) tree | commitdiff
2019-05-15 Andrew ReynoldsFix printing of bvurem (#2963) tree | commitdiff
2019-05-09 Andrew ReynoldsFixes for relational triggers (#2967) tree | commitdiff
2019-04-16 Andrew ReynoldsStratify enumerative instantiation (#2954) tree | commitdiff
2019-04-05 Haniel Barbosafix fp issue (#2940) tree | commitdiff
next