Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-09-02 | Fixes from merge | ajreynol | |
2021-08-31 | Use more robust conversion for arithmetic trichotomy | ajreynol | |
2021-08-31 | Support arith trichotomy in LFSC | ajreynol | |
2021-08-31 | Add support concat unify in LFSC | ajreynol | |
2021-08-04 | Add test_proof_new | ajreynol | |
2021-08-04 | Improved and updated testing scripts | ajreynol | |
2021-07-30 | Add proper conversion for bitblast term, proper printing for bitOf, update ↵ | ajreynol | |
LFSC version | |||
2021-07-30 | Simplify smt2 printer, fix order issue in strings eager reduction, update ↵ | ajreynol | |
LFSC version | |||
2021-06-21 | Merge branch 'master' into proof-new | Haniel Barbosa | |
2021-06-16 | Archive SMT-COMP 2021 run scripts (#6748) | Andres Noetzli | |
This commit copies the run-script-smtcomp-current* scripts to run-script-smtcomp2021* to archive them. | |||
2021-06-14 | Final update to SMT-COMP 2021 options (#6739) | Andres Noetzli | |
This commit: - Disables `--tear-down-incremental=X` for the competition since it currently does not work correctly on master and a fixed version did not show significant benefits. - Changes the occurrences of `--nl-ext` to `--nl-ext=full` because it is now a mode option. - Removes the use of `--bv-assert-input` because the option currently has some issues in incremental mode (#6738) - Removes the use of `--bitblast=eager` for the model validation track because it produces invalid models (#6741) | |||
2021-06-11 | Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new | ajreynol | |
2021-06-10 | smtcomp: Change some BV configs for SQ and INC track. (#6721) | Mathias Preiner | |
2021-06-09 | Update options for SMT-COMP (#6704) | Andres Noetzli | |
This commit removes obsolete options for BV and strings logics, and updates QF_NIA to spend more time on our best configuration. Co-authored-by: Gereon Kremer nafur42@gmail.com Co-authored-by: Mathias Preiner mathias.preiner@gmail.com | |||
2021-06-04 | Format, update LFSC commit | ajreynol | |
2021-06-01 | Update LFSC commit | ajreynol | |
2021-06-01 | Merge branch 'master' of https://github.com/cvc5/cvc5 into proof-new | ajreynol | |
2021-05-30 | Remove invalid options from run scripts (#6645) | Andres Noetzli | |
This commit removes some of the options in the run scripts that are not supported anymore: `--bv-div-zero-const` and `--rewrite-divk`. Both of those options are effectively enabled by default in cvc5. | |||
2021-05-27 | Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new | ajreynol | |
2021-05-27 | Enable new justification heuristic by default (#6613) | Andrew Reynolds | |
This enables the new implementation of justification heuristic by default. Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160. | |||
2021-05-25 | Generalize string reductions to sequences, simplify. | ajreynol | |
2021-05-25 | Use side condition for and elim, simplify policy for assigning assumption ↵ | ajreynol | |
ids, fixes | |||
2021-05-25 | Improved support for datatype testers and updaters in LFSC output | ajreynol | |
2021-05-25 | Drop type annotations on ITE in LFSC | ajreynol | |
2021-05-25 | Minor fix for quantifier skolems | ajreynol | |
2021-05-25 | Fix related to original form of witness skolems in LFSC | ajreynol | |
2021-05-24 | Fix LFSC for nested skolems in purification | ajreynol | |
2021-05-21 | Refactor regular expression unfolding, formalize skolems, working LFSC ↵ | ajreynol | |
translation of RE_UNFOLD_POS | |||
2021-05-21 | Support shared selectors in LFSC proof output | ajreynol | |
2021-05-19 | Use skolem function for shared selectors | ajreynol | |
2021-05-19 | Update LFSC commit | ajreynol | |
2021-05-19 | Minor, update LFSC signature | ajreynol | |
2021-05-17 | Update LFSC signature | ajreynol | |
2021-05-17 | Minor fixes for LFSC conversion | ajreynol | |
2021-05-17 | Constant sequences, more fixes, exclude bad regressions | ajreynol | |
2021-05-17 | LFSC commit | ajreynol | |
2021-05-17 | Simplify indexof reduction, update LFSC sig commit | ajreynol | |
2021-05-14 | More additions for LFSC, ho congruence, missing operators | ajreynol | |
2021-05-14 | Increment lfsc commit | ajreynol | |
2021-05-13 | Increment LFSC commit | ajreynol | |
2021-05-13 | Fixes to LFSC printer | ajreynol | |
2021-05-13 | Fix congruence over quantifiers in LFSC | ajreynol | |
2021-05-13 | Properly print sorts using user names in LFSC, fix pow. | ajreynol | |
2021-05-12 | Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new | ajreynol | |
2021-05-12 | Preliminary draft of changes for SMT comp 2021 (#6522) | Andrew Reynolds | |
Covers improvements to quantifiers. | |||
2021-05-05 | Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new | ajreynol | |
2021-04-28 | Allow Int/Real subtyping in LFSC proofs | ajreynol | |
2021-04-27 | LFSC commit | ajreynol | |
2021-04-27 | Minor fixes, additions to LFSC | ajreynol | |
2021-04-27 | Work on indexed operators in LFSC | ajreynol | |