projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Only run pypi packaging when release is published (#8526)
[cvc5.git]
/
test
/
regress
/
2022-04-01
Haniel Barbosa
[proofs] [alethe] Fix Alethe post-processor (#8525)
tree
|
commitdiff
2022-04-01
Andres Noetzli
[API] Add mode argument for `Solver::blockModel()`...
tree
|
commitdiff
2022-04-01
Andrew Reynolds
Fix sygus-inst when combined with bounded string quanti...
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Handled quoted symbols in indexed operators (#8491)
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Disable minisat variable elimination when a parametric...
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Fix check for whether PI is reduced (#8485)
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Fix lower vs upper bound issue for eager RE conflicts...
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Fix non-termination in the strings rewriter (#8438)
tree
|
commitdiff
2022-03-31
Andrew Reynolds
Fix case of Boolean skolem for ground term E-matching...
tree
|
commitdiff
2022-03-30
Gereon Kremer
Allow for multiple (equal) base model values (#8467)
tree
|
commitdiff
2022-03-30
Mathias Preiner
Exclude competition build for issue8377-resolve-indexed...
tree
|
commitdiff
2022-03-30
Andrew Reynolds
Fix policy for purifying arguments of exp (#8416)
tree
|
commitdiff
2022-03-30
Andrew Reynolds
Fixes for sygus-inst (#8448)
tree
|
commitdiff
2022-03-30
Andrew Reynolds
Fix subtype issue in cegqi arithmetic (#8440)
tree
|
commitdiff
2022-03-30
Andrew Reynolds
Change tuple tokens and update datatypes theory ref...
tree
|
commitdiff
2022-03-30
Mathias Preiner
Rename master branch to main. (#8452)
tree
|
commitdiff
2022-03-29
yoni206
bv-to-int: fix translation of bvneg (#8437)
tree
|
commitdiff
2022-03-29
Andrew Reynolds
Make ProofNodeManager mkScope more robust (#8435)
tree
|
commitdiff
2022-03-29
Andrew Reynolds
Fix issue related to use of Boolean term variable for...
tree
|
commitdiff
2022-03-29
Clark Barrett
Fix for issue 5925: constant arrays should be nonlinear...
tree
|
commitdiff
2022-03-28
Mathias Preiner
Rename get-interpol to get-interpolant. (#8424)
tree
|
commitdiff
2022-03-26
yoni206
Separating produce-interpols from the mode of interpola...
tree
|
commitdiff
2022-03-26
Andrew Reynolds
Fix spurious assertion failure (#8404)
tree
|
commitdiff
2022-03-26
Andrew Reynolds
More minor cleaning of options (#8401)
tree
|
commitdiff
2022-03-26
Andrew Reynolds
Fixes for API kind documentation (#8397)
tree
|
commitdiff
2022-03-25
Andres Noetzli
[Parser] Fix resolution of indexed symbols (#8383)
tree
|
commitdiff
2022-03-25
Haniel Barbosa
[proofs] [sat] Have SAT solver communicate whether...
tree
|
commitdiff
2022-03-25
Andrew Reynolds
Update checkSynth and checkSynthNext to return SynthRes...
tree
|
commitdiff
2022-03-25
Andrew Reynolds
Change output of abduction/interpolation for failed...
tree
|
commitdiff
2022-03-25
Andrew Reynolds
Properly guard commands in the SyGuS API (#8390)
tree
|
commitdiff
2022-03-25
Andrew Reynolds
Recategorize options (#8386)
tree
|
commitdiff
2022-03-24
Haniel Barbosa
[unsat-cores] [sat-proof] Fix open proofs due to theory...
tree
|
commitdiff
2022-03-23
Andrew Reynolds
Clean options (#8309)
tree
|
commitdiff
2022-03-23
Andrew Reynolds
Make IDOF_MAX rewrite only apply when all children...
tree
|
commitdiff
2022-03-23
mudathirmahgoub
Fix cvc5-projects issue 497 (#8331)
tree
|
commitdiff
2022-03-23
Andrew Reynolds
Fix non-termination issue in sygus enumerator (#8340)
tree
|
commitdiff
2022-03-22
Andrew Reynolds
Fixes for witness terms appearing in CEGQI instantiatio...
tree
|
commitdiff
2022-03-16
Andres Noetzli
Remove unused files in `regress0` (#8325)
tree
|
commitdiff
2022-03-16
Aina Niemetz
First step towards refactoring regression tests. (...
tree
|
commitdiff
2022-03-16
mudathirmahgoub
Add regression for cvc5-projects issue 490 (#8317)
tree
|
commitdiff
2022-03-16
Mathias Preiner
run_regression: Make sure to strip trailing whitespaces...
tree
|
commitdiff
2022-03-16
Andrew Reynolds
Fix getModelValue for arithmetic (#8316)
tree
|
commitdiff
2022-03-16
Andrew Reynolds
Ensure trusted steps are given for skolem lemmas when...
tree
|
commitdiff
2022-03-15
Andrew Reynolds
Make learned literal computation more robust (#8308)
tree
|
commitdiff
2022-03-15
Andres Noetzli
[BV] Fix strategy for rewriting `bvnot` (#8297)
tree
|
commitdiff
2022-03-15
Andrew Reynolds
Fix issues involving multiple sources of model substitu...
tree
|
commitdiff
2022-03-15
mudathirmahgoub
Add skolem lemmas for bags card terms (#7995)
tree
|
commitdiff
2022-03-15
Andrew Reynolds
Fix to consider leafs of theory sets to be variables...
tree
|
commitdiff
2022-03-15
Andrew Reynolds
Simplify reductions for set and bag choose (#8304)
tree
|
commitdiff
2022-03-14
Andrew Reynolds
Fixes for skolem definition management (#8301)
tree
|
commitdiff
2022-03-14
Andrew Reynolds
Remove unecessary methods from the API (#8260)
tree
|
commitdiff
2022-03-14
Andrew Reynolds
Add rewrite for allchar beneath union + star (#8299)
tree
|
commitdiff
2022-03-14
Andrew Reynolds
Run preprocess rewrite on equalities until fixed point...
tree
|
commitdiff
2022-03-12
Andrew Reynolds
Introduce new splitting inference in sets + cardinality...
tree
|
commitdiff
2022-03-11
Andrew Reynolds
Remove old decision justification heurstic (#8275)
tree
|
commitdiff
2022-03-11
Andrew Reynolds
Consider APPLY_CONSTRUCTOR applied to values to be...
tree
|
commitdiff
2022-03-11
Andrew Reynolds
Fix reduction for arc trig functions (#8289)
tree
|
commitdiff
2022-03-10
Andrew Reynolds
Fix theoryOf call in get equality status (#8279)
tree
|
commitdiff
2022-03-10
Andrew Reynolds
Eliminate unecessary datatype options (#8280)
tree
|
commitdiff
2022-03-10
mudathirmahgoub
Fix cvc5-projects issue 475 (#8278)
tree
|
commitdiff
2022-03-10
Andrew Reynolds
Add output -o pre-asserts (#8270)
tree
|
commitdiff
2022-03-10
Andrew Reynolds
Disable timing out regressions (#8273)
tree
|
commitdiff
2022-03-10
Mathias Preiner
Fix regression errors for arm64 nightlies. (#8268)
tree
|
commitdiff
2022-03-09
Gereon Kremer
Rename expert statistics to internal, add documentation...
tree
|
commitdiff
2022-03-09
Gereon Kremer
Clear obsolete pending lemmas in arithmetic (#8236)
tree
|
commitdiff
2022-03-09
Andrew Reynolds
Add regression for fixed issue 6700 (#8265)
tree
|
commitdiff
2022-03-08
Andrew Reynolds
Do not expand APPLY_SELECTOR (#8174)
tree
|
commitdiff
2022-03-08
Andrew Reynolds
Guard another case of non-termination in quantifiers...
tree
|
commitdiff
2022-03-08
Gereon Kremer
Make one CI job not use libpoly (#8261)
tree
|
commitdiff
2022-03-08
Andrew Reynolds
Eliminate shadowing in the quantifiers rewriter (#8244)
tree
|
commitdiff
2022-03-07
Gereon Kremer
Try harder to show that a RAN is rational (#8230)
tree
|
commitdiff
2022-03-06
Andres Noetzli
Disallow models with `--arrays-weak-equiv` (#8217)
tree
|
commitdiff
2022-03-05
Andrew Reynolds
Make seq.unit robust wrt subtyping (#8209)
tree
|
commitdiff
2022-03-05
Gereon Kremer
Add regressions for fixed issue (#8237)
tree
|
commitdiff
2022-03-05
Andrew Reynolds
Enable NL tangent planes by default (#8233)
tree
|
commitdiff
2022-03-04
Gereon Kremer
Remove spurious assertion in linear solver (#8231)
tree
|
commitdiff
2022-03-04
Gereon Kremer
Guard recursion into terms during substitution in arith...
tree
|
commitdiff
2022-03-04
Andrew Reynolds
Fix rewrite rule synthesis for 0-ary operators (#8221)
tree
|
commitdiff
2022-03-04
Andrew Reynolds
Logic exception when using solution filtering for non...
tree
|
commitdiff
2022-03-04
Andrew Reynolds
Add regressions for fixed projects issues (#8228)
tree
|
commitdiff
2022-03-04
Andrew Reynolds
Add support for get learned literals in the API (#8099)
tree
|
commitdiff
2022-03-03
Andrew Reynolds
Throw logic exception if a transcendental function...
tree
|
commitdiff
2022-03-03
Andrew Reynolds
Add regression for fixed issue (#8213)
tree
|
commitdiff
2022-03-03
Gereon Kremer
Fix rewriting of mixed-integer atoms (#8214)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Fix issue with dropping non-reduced sine terms (#8211)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Fix models involving cardinality of sets of finite...
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Always purify universe from set minus (#8201)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Fix incorrect assertion in prop engine proofs (#8204)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Clean usage of options in regressions (#8190)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Improve error message when not using strings-exp (...
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Add regressions for fixed issues (#8202)
tree
|
commitdiff
2022-03-02
Gereon Kremer
Prune spurious roots in lazard evaluation of coverings...
tree
|
commitdiff
2022-03-01
Andrew Reynolds
Fix issue involving dropped purification lemmas for...
tree
|
commitdiff
2022-03-01
Andrew Reynolds
Disable regression (#8191)
tree
|
commitdiff
2022-03-01
Andres Noetzli
[BV] Fix rewriter policy for `bvneg` (#8196)
tree
|
commitdiff
2022-03-01
Gereon Kremer
Rename cad to coverings (#8187)
tree
|
commitdiff
2022-02-28
Andres Noetzli
[Seq/Model] Do not enumerate elements of constants...
tree
|
commitdiff
2022-02-28
Andrew Reynolds
Fix special casing for PI in model value (#8189)
tree
|
commitdiff
2022-02-28
Andrew Reynolds
Preserve model values for exact sine points (#8188)
tree
|
commitdiff
2022-02-28
Andrew Reynolds
Track names for witness terms in model (#8184)
tree
|
commitdiff
next