projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Remove quantifiers regression from decision folder (#5830)
[cvc5.git] / test / regress / CMakeLists.txt
2021-02-02 Andrew ReynoldsRemove quantifiers regression from decision folder... blob | commitdiff | raw
2021-02-02 Haniel Barbosa[proof-new] Fix bug in expansion of MACRO_RESOLUTION... blob | commitdiff | raw | diff to current
2021-01-30 Andrew ReynoldsFix unguarded call to get representative (#5838) blob | commitdiff | raw | diff to current
2021-01-29 mudathirmahgoubAdd bag inferences for operators: intersection, duplica... blob | commitdiff | raw | diff to current
2021-01-28 Andrew ReynoldsAlways theory-preprocess lemmas (#5817) blob | commitdiff | raw | diff to current
2021-01-27 Andrew Reynolds(proof-new) Improvements to quantifiers engine and... blob | commitdiff | raw | diff to current
2021-01-26 Andrew ReynoldsRemove deprecated quantifiers modules (#5820) blob | commitdiff | raw | diff to current
2021-01-26 Haniel BarbosaReestablishing support for define-sort (#5810) blob | commitdiff | raw | diff to current
2021-01-25 mudathirmahgoubRefactor bags::SolverState (#5783) blob | commitdiff | raw | diff to current
2021-01-25 Andrew ReynoldsEnsure uses of ground terms in triggers are preprocesse... blob | commitdiff | raw | diff to current
2021-01-20 Andrew ReynoldsFix corner case of wrongly applied selector as trigger... blob | commitdiff | raw | diff to current
2021-01-20 Andrew ReynoldsDo not track processed in remove term formulas loop... blob | commitdiff | raw | diff to current
2021-01-20 Aina NiemetzSMT2 parser: Do not add non-linear symbols for linear... blob | commitdiff | raw | diff to current
2021-01-20 Andrew ReynoldsUse arbitrary ground term assignment for sorts where... blob | commitdiff | raw | diff to current
2021-01-15 Andrew ReynoldsImplement --no-strings-lazy-pp as a preprocessing pass... blob | commitdiff | raw | diff to current
2021-01-13 Andrew ReynoldsDo not call ppRewrite on Boolean equalities (#5762) blob | commitdiff | raw | diff to current
2021-01-12 yoni206Foreign theory rewrite option (#5763) blob | commitdiff | raw | diff to current
2021-01-11 Andrew ReynoldsRemove extended rewrite for arithmetic (#5760) blob | commitdiff | raw | diff to current
2021-01-08 mudathirmahgoubAdd bags inference generator (#5731) blob | commitdiff | raw | diff to current
2021-01-07 Gereon KremerMake sure polynomials are properly factorized in nl... blob | commitdiff | raw | diff to current
2021-01-05 yoni206Adding str.len to triggers (#5746) blob | commitdiff | raw | diff to current
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716) blob | commitdiff | raw | diff to current
2020-12-22 Andrew ReynoldsMove slow regression to regress3 (#5715) blob | commitdiff | raw | diff to current
2020-12-18 Alex OzdemirBugfix: proofs for props of non-normal arith lits ... blob | commitdiff | raw | diff to current
2020-12-17 Andrew ReynoldsSimplify and fix check models (#5685) blob | commitdiff | raw | diff to current
2020-12-16 Andrew ReynoldsMark quantifier instantiations as needs justify (#5684) blob | commitdiff | raw | diff to current
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) blob | commitdiff | raw | diff to current
2020-12-14 Andrew ReynoldsFix SAT-context dependent issue in strings preregistrat... blob | commitdiff | raw | diff to current
2020-12-11 yoni206bv-to-int: new tests from an issue (#5654) blob | commitdiff | raw | diff to current
2020-12-11 Andrew ReynoldsFix length assumption for deq norm emp rule (#5623) blob | commitdiff | raw | diff to current
2020-12-10 Andrew ReynoldsRefactor regressions (#5639) blob | commitdiff | raw | diff to current
2020-12-09 Andrew ReynoldsRemove obsolete regressions (#5633) blob | commitdiff | raw | diff to current
2020-12-09 Andrew ReynoldsEnsure CEGQI is applied for parametric datatypes when... blob | commitdiff | raw | diff to current
2020-12-08 Gereon KremerAdd regression from #1978. (#5552) blob | commitdiff | raw | diff to current
2020-12-08 Abdalrhman MohamedFix a bug with synth-fun printer (#5512) blob | commitdiff | raw | diff to current
2020-12-08 yoni206bv-to-int: Expand definitions of bvudiv and bvurem... blob | commitdiff | raw | diff to current
2020-12-08 Andrew ReynoldsMake term indices in the strings base solver aware... blob | commitdiff | raw | diff to current
2020-12-08 Andrew ReynoldsProper implementation of expand definitions for sequenc... blob | commitdiff | raw | diff to current
2020-12-08 Andrew ReynoldsFix collect model values for sequences of sequences... blob | commitdiff | raw | diff to current
2020-12-08 Mathias PreinerDisable algebraic BV subtheory by default and make... blob | commitdiff | raw | diff to current
2020-12-07 Andrew ReynoldsFix and reenable fact vs lemma optimization in datatype... blob | commitdiff | raw | diff to current
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier... blob | commitdiff | raw | diff to current
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... blob | commitdiff | raw | diff to current
2020-12-07 Gereon KremerAdd regression from #4927 (#5556) blob | commitdiff | raw | diff to current
2020-12-03 Gereon KremerUse mkAnd where the number of children may be less... blob | commitdiff | raw | diff to current
2020-12-03 yoni206Models as (#5581) blob | commitdiff | raw | diff to current
2020-12-02 Aina NiemetzFix RoundingMode mapping in API. (#5578) blob | commitdiff | raw | diff to current
2020-12-02 Gereon KremerAdd regressions from #3687. (#5553) blob | commitdiff | raw | diff to current
2020-12-02 Andrew ReynoldsFix issues related to model declarations (#5560) blob | commitdiff | raw | diff to current
2020-12-01 Andres NoetzliImprove rewriting of str.<= (#4848) blob | commitdiff | raw | diff to current
2020-12-01 Gereon KremerAdd regressions from #5099 (#5557) blob | commitdiff | raw | diff to current
2020-12-01 Gereon KremerAdd regression for #4335. (#5554) blob | commitdiff | raw | diff to current
2020-12-01 Gereon KremerAdd regressions for #4707. (#5555) blob | commitdiff | raw | diff to current
2020-12-01 Andrew ReynoldsMore fixes for quantifier elimination (#5533) blob | commitdiff | raw | diff to current
2020-11-26 Gereon KremerMake CAD solver work for empty set of assertions (... blob | commitdiff | raw | diff to current
2020-11-26 Andrew ReynoldsDisable fact vs lemma optimization in datatypes for... blob | commitdiff | raw | diff to current
2020-11-25 Andrew ReynoldsAdd regressions for closed issues (#5526) blob | commitdiff | raw | diff to current
2020-11-23 Andrew ReynoldsFix regular expression consume for nested star (#5518) blob | commitdiff | raw | diff to current
2020-11-23 Andrew ReynoldsFix quantifiers scope issue in strings preprocessor... blob | commitdiff | raw | diff to current
2020-11-20 Andrew ReynoldsFix remove term formula policy for terms beneath quanti... blob | commitdiff | raw | diff to current
2020-11-20 Andrew ReynoldsSupport nested quantifier elimination for get-qe comman... blob | commitdiff | raw | diff to current
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... blob | commitdiff | raw | diff to current
2020-11-19 Andrew ReynoldsFix issues related to eliminating extended arithmetic... blob | commitdiff | raw | diff to current
2020-11-18 Andrew ReynoldsDisable slow nl regression (#5467) blob | commitdiff | raw | diff to current
2020-11-18 Andrew ReynoldsDo not expand definitions of extended arithmetic operat... blob | commitdiff | raw | diff to current
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) blob | commitdiff | raw | diff to current
2020-11-14 Andrew ReynoldsFix double conflict in extended string solver (#5435) blob | commitdiff | raw | diff to current
2020-11-13 Andrew ReynoldsMake regular expression difference left associative... blob | commitdiff | raw | diff to current
2020-11-11 Andrew ReynoldsFix preregistration in TheorySep before declare-heap... blob | commitdiff | raw | diff to current
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on... blob | commitdiff | raw | diff to current
2020-11-09 Andrew ReynoldsDo not regress explanations of datatype lemmas (#5376) blob | commitdiff | raw | diff to current
2020-11-06 mudathirmahgoubFix issue #5342 (#5349) blob | commitdiff | raw | diff to current
2020-11-04 Andres NoetzliAdd constants from equality engine evaluation to model... blob | commitdiff | raw | diff to current
2020-11-03 Andrew ReynoldsReset built model flag at presolve in nonlinear (#5386) blob | commitdiff | raw | diff to current
2020-11-02 Andrew ReynoldsUpdate strings proxy variable map to be context indepen... blob | commitdiff | raw | diff to current
2020-10-28 Andrew ReynoldsFixes for unconstrained variables in nonlinear model... blob | commitdiff | raw | diff to current
2020-10-28 Andrew ReynoldsConvert symbol table from Expr-level to Term-level... blob | commitdiff | raw | diff to current
2020-10-24 mudathirmahgoubFix issue 5271 (#5335) blob | commitdiff | raw | diff to current
2020-10-23 Andrew ReynoldsFix related to preregistering boolean term variables... blob | commitdiff | raw | diff to current
2020-10-22 mudathirmahgoubFix issue 5309 (#5327) blob | commitdiff | raw | diff to current
2020-10-20 yoni206Expand `seq.nth` lazily (#5287) blob | commitdiff | raw | diff to current
2020-10-16 Andrew ReynoldsCatch more cases of nested recursion in datatypes ... blob | commitdiff | raw | diff to current
2020-10-16 yoni206bv2int: caching introduced terms (#5283) blob | commitdiff | raw | diff to current
2020-10-14 yoni206bv2int: implementing the iand-sum mode (#5265) blob | commitdiff | raw | diff to current
2020-10-14 yoni206bv2int: rewritings and unsat cores (#5263) blob | commitdiff | raw | diff to current
2020-10-12 Andrew ReynoldsRemove uf-ss-totality option (#5251) blob | commitdiff | raw | diff to current
2020-10-12 Andrew ReynoldsEnsure uninterpreted sort owner is UF if uf-ho or finit... blob | commitdiff | raw | diff to current
2020-10-09 Andres Noetzlireset-assertions: Remove all non-global symbols in... blob | commitdiff | raw | diff to current
2020-10-07 Gereon KremerMake sure conflicts are not rewritten (in arithmetic... blob | commitdiff | raw | diff to current
2020-10-06 yoni206bv-to-int: change order of passes (#5208) blob | commitdiff | raw | diff to current
2020-09-29 Andrew ReynoldsReset assertions on resetAssertions (#5153) blob | commitdiff | raw | diff to current
2020-09-29 Andrew ReynoldsDisable regression that is timing out (#5142) blob | commitdiff | raw | diff to current
2020-09-27 Andrew ReynoldsFix sygus quantifier elimination preprocess for multipl... blob | commitdiff | raw | diff to current
2020-09-26 Andrew ReynoldsUse original quantified formula for single invocation... blob | commitdiff | raw | diff to current
2020-09-24 Andrew ReynoldsModify lemma vs fact policy for datatype equalities... blob | commitdiff | raw | diff to current
2020-09-23 Andrew ReynoldsDisable cegqi-bv when using sygus (#5124) blob | commitdiff | raw | diff to current
2020-09-23 yoni206bv2int: new options for bvand translation (#5096) blob | commitdiff | raw | diff to current
2020-09-23 Andrew ReynoldsAllow E-matching by default when strings are enabled... blob | commitdiff | raw | diff to current
2020-09-23 Abdalrhman MohamedRefactor Commands to use the Public API. (#5105) blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... blob | commitdiff | raw | diff to current
next