projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
add bag.fold operator (#7718)
[cvc5.git]
/
test
/
regress
/
regress2
/
2021-11-08
Aina Niemetz
sets: Rename kinds with a more consistent naming scheme...
tree
|
commitdiff
2021-10-28
Abdalrhman Mohamed
Fix `(set-info <sexpr>)` parsing and printing bugs...
tree
|
commitdiff
2021-10-25
Andrew Reynolds
Add new method for enumerating unsat queries with SyGuS...
tree
|
commitdiff
2021-10-07
Andrew Reynolds
Make the cardinality of the alphabet of strings configu...
tree
|
commitdiff
2021-09-22
Mathias Preiner
Remove CVC language support (#7219)
tree
|
commitdiff
2021-09-21
Andres Noetzli
Fix 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 Reynolds
Fix issues with cyclic proofs due to double SYMM applic...
tree
|
commitdiff
2021-08-26
Gereon Kremer
Improve integration of nonlinear arithmetic into the...
tree
|
commitdiff
2021-08-02
Mathias Preiner
bv: 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 Reynolds
Integrate central equality engine approach into theory...
tree
|
commitdiff
2021-07-27
Andres Noetzli
Add regression for fixed `str.indexof_re` issue (#6938)
tree
|
commitdiff
2021-07-01
Andrew Reynolds
Add recursive function definitions to subsolver in...
tree
|
commitdiff
2021-06-16
Aina Niemetz
Make symfpu a required dependency. (#6749)
tree
|
commitdiff
2021-06-11
Haniel Barbosa
Better support for HOL parsing and set up (#6697)
tree
|
commitdiff
2021-06-10
Andrew Reynolds
Ensure bv2nat and int2bv are not rewritten when using...
tree
|
commitdiff
2021-06-04
Andres Noetzli
Fix handling of start index in `str.indexof_re` (#6674)
tree
|
commitdiff
2021-06-03
yoni206
Renaming pow2 to p2 in regression tests (#6675)
tree
|
commitdiff
2021-06-02
Aina Niemetz
Remove redundant logic ALL_SUPPORTED. (#6664)
tree
|
commitdiff
2021-05-28
Andres Noetzli
Disable `--jh-rlv-order` for slow regressions (#6633)
tree
|
commitdiff
2021-05-27
Andres Noetzli
Fix `str.replace_re` and `str.replace_re_all` (#6615)
tree
|
commitdiff
2021-05-27
Andrew Reynolds
Enable new justification heuristic by default (#6613)
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Fix tests of unsat cores (#6593)
tree
|
commitdiff
2021-05-19
Haniel Barbosa
Change the default unsat cores (#6571)
tree
|
commitdiff
2021-05-18
Andres Noetzli
Fix `collectEmptyEqs()` in string utils (#6562)
tree
|
commitdiff
2021-05-17
Gereon Kremer
Improve integration of CAD with nl-Ext (#6542)
tree
|
commitdiff
2021-05-07
Aina Niemetz
Move slow regressions and update guidelines. (#6508)
tree
|
commitdiff
2021-05-06
Andrew Reynolds
Discard duplicate terms in patterns (#6501)
tree
|
commitdiff
2021-04-27
Andrew Reynolds
Move slow regression to regress3 (#6451)
tree
|
commitdiff
2021-04-25
Andrew Reynolds
More check models (#6439)
tree
|
commitdiff
2021-04-24
Andrew Reynolds
Improve getValue for non-evaluated operators (#6436)
tree
|
commitdiff
2021-04-22
Andrew Reynolds
Fix models for sygus-inference, bv2int, real2int (...
tree
|
commitdiff
2021-04-22
Haniel Barbosa
Reconciling 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 Preiner
Remove SMT-LIB 2.5 and 2.0 support. (#6068)
tree
|
commitdiff
2021-01-20
Aina Niemetz
SMT2 parser: Do not add non-linear symbols for linear...
tree
|
commitdiff
2020-12-17
Andrew Reynolds
Simplify and fix check models (#5685)
tree
|
commitdiff
2020-12-10
Andrew Reynolds
Refactor regressions (#5639)
tree
|
commitdiff
2020-12-08
Gereon Kremer
Add regression from #1978. (#5552)
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Do not expand theory definitions at the beginning of...
tree
|
commitdiff
2020-12-02
Gereon Kremer
Add regressions from #3687. (#5553)
tree
|
commitdiff
2020-12-01
Gereon Kremer
Add regressions for #4707. (#5555)
tree
|
commitdiff
2020-11-23
Andrew Reynolds
Change UF ho to ppRewrite instead of expand definition...
tree
|
commitdiff
2020-11-10
Andrew Reynolds
Do not mark extended functions as reduced based on...
tree
|
commitdiff
2020-11-09
Andrew Reynolds
Do not regress explanations of datatype lemmas (#5376)
tree
|
commitdiff
2020-10-14
yoni206
bv2int: implementing the iand-sum mode (#5265)
tree
|
commitdiff
2020-10-14
yoni206
bv2int: rewritings and unsat cores (#5263)
tree
|
commitdiff
2020-10-06
yoni206
bv-to-int: change order of passes (#5208)
tree
|
commitdiff
2020-09-23
yoni206
bv2int: new options for bvand translation (#5096)
tree
|
commitdiff
2020-09-16
yoni206
bv2int: support models in tests (#5068)
tree
|
commitdiff
2020-09-10
yoni206
bv2int: improvement in lazy failures (#5020)
tree
|
commitdiff
2020-09-03
yoni206
Changing the handled operators in bv2int preprocessing...
tree
|
commitdiff
2020-08-28
yoni206
Incremental support for bv_to_int (#4967)
tree
|
commitdiff
2020-08-24
Mathias Preiner
Increase 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 Reynolds
Add support for string/sequence update (#4725)
tree
|
commitdiff
2020-07-11
yoni206
Changing bv_to_int options (#4721)
tree
|
commitdiff
2020-07-09
Andrew Reynolds
Disable unsat cores in timeout regression (#4713)
tree
|
commitdiff
2020-06-10
Andres Noetzli
Add support for str.replace_re/str.replace_re_all ...
tree
|
commitdiff
2020-05-23
Andrew Reynolds
Refactor operator elimination in arithmetic (#4519)
tree
|
commitdiff
2020-05-19
Andres Noetzli
Make SolveEq and PlusCombineLikeTerms idempotent (...
tree
|
commitdiff
2020-05-02
Andrew Reynolds
Move slow regression to regress3 (#4430)
tree
|
commitdiff
2020-04-28
Andrew Reynolds
Support the SMT-LIB Unicode string standard by default...
tree
|
commitdiff
2020-04-28
Andrew Reynolds
Update cardinality in strings to unicode standard ...
tree
|
commitdiff
2020-04-22
Abdalrhman Mohamed
Convert V2.5 SMT regressions to V2.6. (#4319)
tree
|
commitdiff
2020-04-21
Andrew Reynolds
Make option names related to CEGQI consistent (#4316)
tree
|
commitdiff
2020-04-19
Andrew Reynolds
Disable unsat cores on nec regression (#4330)
tree
|
commitdiff
2020-04-17
Mathias Preiner
SyGuS instantiation quantifiers module (#3910)
tree
|
commitdiff
2020-04-12
Andrew Reynolds
Move slow nl regression to regress3 (#4276)
tree
|
commitdiff
2020-04-01
Aina Niemetz
Rename checkValid/query to checkEntailed. (#4191)
tree
|
commitdiff
2020-03-31
Andrew Reynolds
Fixing regressions (#4189)
tree
|
commitdiff
2020-03-30
Andrew Reynolds
Support indexed operators re.loop and re.^ (#4167)
tree
|
commitdiff
2020-03-22
Abdalrhman Mohamed
Convert V1 Sygus files to V2. (#4136)
tree
|
commitdiff
2020-03-19
yoni206
Bv2int fail on demand
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Add options for nec regression (#4056)
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Switch to Nodes for conjecture generator (#4026)
tree
|
commitdiff
2020-03-06
Andrew Reynolds
Remove tester name from APIs (#3929)
tree
|
commitdiff
2020-03-06
Andrew Reynolds
Support default sygus grammar construction for sets...
tree
|
commitdiff
2020-02-25
yoni206
bv_to_int preprocessing pass
tree
|
commitdiff
2020-02-03
Andrew Reynolds
Example inference utility (#3670)
tree
|
commitdiff
2020-01-14
Andres Noetzli
Disable unsat cores for regression that times out ...
tree
|
commitdiff
2020-01-07
Andrew Reynolds
Update any-constant and normalization policies for...
tree
|
commitdiff
2019-12-12
Andrew Reynolds
Make CEGIS sampling robust to non-vanilla CEGIS (#3559)
tree
|
commitdiff
2019-12-05
Andrew Reynolds
Refactor mode options for Unif+PI (#3531)
tree
|
commitdiff
2019-09-19
Andrew Reynolds
Support context-(in)dependent decision strategies....
tree
|
commitdiff
2019-09-18
Andrew Reynolds
Decouple fmf-bound and finite-model-find (#3297)
tree
|
commitdiff
2019-09-06
Mathias Preiner
Remove SMT1 parser. (#3228)
tree
|
commitdiff
2019-09-04
Mathias Preiner
Remove duplicate regression tests. (#3227)
tree
|
commitdiff
2019-08-30
Andres Noetzli
Better 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 Reynolds
Support default sygus grammar for strings (#3148)
tree
|
commitdiff
2019-07-31
Haniel Barbosa
Parsing THF and adding several regressions (#3131)
tree
|
commitdiff
2019-06-10
Andrew Reynolds
Optimization for negative concatenation membership...
tree
|
commitdiff
2019-06-04
Andres Noetzli
Enable proof checking for QF_LRA benchmarks (#2928)
tree
|
commitdiff
2019-05-15
Andrew Reynolds
Fix printing of bvurem (#2963)
tree
|
commitdiff
2019-05-09
Andrew Reynolds
Fixes for relational triggers (#2967)
tree
|
commitdiff
2019-04-16
Andrew Reynolds
Stratify enumerative instantiation (#2954)
tree
|
commitdiff
2019-04-05
Haniel Barbosa
fix fp issue (#2940)
tree
|
commitdiff
next