summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings
AgeCommit message (Expand)Author
2021-09-22Remove CVC language support (#7219)Mathias Preiner
2021-08-23Purify substitutions in strings proof reconstruction (#7035)Andrew Reynolds
2021-07-05[Strings] Fix incorrect rewrite (#6837)Andres Noetzli
2021-06-05Remove unwanted side effects in `SPLIT_EQ_STRIP_L` (#6689)Andres Noetzli
2021-06-04Fix handling of start index in `str.indexof_re` (#6674)Andres Noetzli
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2021-06-02Make `STRINGS_CTN_DECOMPOSE` an explicit conflict (#6663)Andres Noetzli
2021-05-27`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts (#6632)Andres Noetzli
2021-05-27Fix `str.replace_re` and `str.replace_re_all` (#6615)Andres Noetzli
2021-05-24Fix re-elim length requirement for symbolic RE memberships (#6609)Andrew Reynolds
2021-05-19Fix positive contains indexof rewrites for empty string second argument (#6566)Andrew Reynolds
2021-05-17Fix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites (#6550)Andres Noetzli
2021-05-12Ensure sequences of Booleans generate Boolean term variable skolems when appl...Andrew Reynolds
2021-04-02Fix case where RE unfolding generates a trivially true lemma (#6267)Andrew Reynolds
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2021-02-19Fix rewrite for contains over replace (#5924)Andrew Reynolds
2021-02-11Fix spurious assertion failure in regexp normalization (#5852)Andrew Reynolds
2021-02-08Fix disequality between seq.unit terms (#5880)Andrew Reynolds
2021-01-15Implement --no-strings-lazy-pp as a preprocessing pass (#5777)Andrew Reynolds
2020-12-10Refactor regressions (#5639)Andrew Reynolds
2020-12-08Make term indices in the strings base solver aware of types (#5589)Andrew Reynolds
2020-12-01Improve rewriting of str.<= (#4848)Andres Noetzli
2020-11-14Fix double conflict in extended string solver (#5435)Andrew Reynolds
2020-11-12Make regular expression difference left associative (#5430)Andrew Reynolds
2020-09-18[Strings] Fix extended equality rewriter (#5092)Andres Noetzli
2020-08-19Add strings-exp to regression (#4923)Andrew Reynolds
2020-08-19Require `--strings-exp` when using `str.substr` (#4916)Andres Noetzli
2020-08-19Changes assertion (about maximum set cardinality) to an exception. (#4907)Gereon Kremer
2020-08-01Ensure strict length constraint for decompose rule (#4821)Andres Noetzli
2020-06-30Fix normal form for re.comp (#4676)Andrew Reynolds
2020-06-28Fix non-termination issues in simpleRegExpConsume (#4667)Andrew Reynolds
2020-05-22(proof-new) Add rewrite corresponding to regular expression inclusion (#4513)Andrew Reynolds
2020-05-20Normal form equality conflicts and uniqueness check (#4497)Andrew Reynolds
2020-04-28Support the SMT-LIB Unicode string standard by default (#4378)Andrew Reynolds
2020-04-22Reinstantiate support for conjunctions in facts (#4377)Andres Noetzli
2020-03-31Support char smt-lib syntax (#4188)Andrew Reynolds
2020-03-30Support indexed operators re.loop and re.^ (#4167)Andrew Reynolds
2020-03-27Support unicode internal representation and escape sequences (#3852)Andrew Reynolds
2020-03-19Only apply testConstStringInRegExp to const regexp (#4120)Andres Noetzli
2020-02-28Add support for str.from_code (#3829)Andres Noetzli
2020-02-27Fix large models for strings (#3835)Andrew Reynolds
2020-02-26Add support for is_digit and regular expression difference (#3828)Andrew Reynolds
2020-02-26Basic support for regular expression complement (#3437)Andrew Reynolds
2020-02-21Simple changes towards unicode string standard (#3791)Andrew Reynolds
2020-01-29Fix isLeq function in String utility (#3659)Andrew Reynolds
2019-12-23Initial support for string reverse (#3581)Andrew Reynolds
2019-12-05Bi-directional unrolling of R* regular expressions (#3532)Andres Noetzli
2019-12-01Ensure quantifiers options are set with --no-strings-lazy-pp (#3515)Andrew Reynolds
2019-11-27 Fix indexof range lemma (#3499)Andrew Reynolds
2019-10-08[CVC Parser] Add support for regular expressions (#3346)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback