summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Expand)Author
2019-09-13Disallow let in sygus grammars, check for free variables in sygus constructor...Andrew Reynolds
2019-09-12 Fix default grammar construction for arrays when no free variables are prese...Andrew Reynolds
2019-09-11Fix constructor type printing (#3246)Andrew Reynolds
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
2019-09-04Remove duplicate regression tests. (#3227)Mathias Preiner
2019-08-29Better heuristic for str.code/re.range (#3220)Andres Noetzli
2019-08-29Infer conflicts based on regular expression inclusion (#3234)Andres Noetzli
2019-08-23 Infer emptiness instead of splitting when a string equality rewrites to a co...Andrew Reynolds
2019-08-23Exclude redundant lemmas when tracking inst lemmas. (#3210)Andrew Reynolds
2019-08-23Update dynamic splitting strategy for quantifiers (#3162)Andrew Reynolds
2019-08-22 Local substitutions for context-depdendent simplification in strings (#3204)Andrew Reynolds
2019-08-20Fixes for sygus inference on quantifier free problems (#3202)Andrew Reynolds
2019-08-18Context-independent regular expression unfolding (#3168)Andrew Reynolds
2019-08-14 Update to standard implementation of getting free variables (#3175)Andrew Reynolds
2019-08-13Add string rewrite involving allchar stars (#3167)Andrew Reynolds
2019-08-13Properly implement logic info for separation logic (#3176)Andrew Reynolds
2019-08-13Implement check abduct feature (#3152)Andrew Reynolds
2019-08-08Fix issues with Ninja build system and add configure option. (#3166)Mathias Preiner
2019-08-06Properly parse qualified identifiers (#3111)Andrew Reynolds
2019-08-04Fix regression script for incremental SMT-LIB v2 benchmarks. (#3155)Mathias Preiner
2019-08-02Update CaDiCaL to version 1.0.3. (#3137)Mathias Preiner
2019-08-02Flip the polarity of the argument of get-abduct (#3153)Andrew Reynolds
2019-08-02Remove simplification specialized for sygus si solution reconstruction (#3147)Andrew Reynolds
2019-08-02Support default sygus grammar for strings (#3148)Andrew Reynolds
2019-08-02Fix solution filtering for streaming abducts (#3143)Andrew Reynolds
2019-08-01Enable sygus logic when produce-abducts is true (#3144)Andrew Reynolds
2019-08-01 Regular expression intersection modes (#3134)Andrew Reynolds
2019-07-31Parsing THF and adding several regressions (#3131)Haniel Barbosa
2019-07-30Minor improvement for rewriter for str.replace (#3124)Andrew Reynolds
2019-07-30 Handle RE intersections modulo equality (#3120)Andrew Reynolds
2019-07-30Remove hard coded option for TPTP regressions in run_regression (#3128)Haniel Barbosa
2019-07-29Model blocker feature (#3112)Andrew Reynolds
2019-07-29Support get-abduct smt2 command (#3122)Andrew Reynolds
2019-07-24 Fix null node when using no-strings-lazy-pp (#3114)Andrew Reynolds
2019-07-23Fix sygus datatype parsing in sygus v1 format (#3113)Andrew Reynolds
2019-07-19Fixes for sygus with datatypes (#3103)Andrew Reynolds
2019-07-19Fix case of unfolding negative membership in reg exp concatenation (#3101)Andrew Reynolds
2019-07-18Basic rewrites for tolower/toupper (#3095)Andrew Reynolds
2019-07-16Add support for str.tolower and str.toupper (#3092)Andrew Reynolds
2019-07-15 Add string rewrite to distribute character stars over concatenation (#3091)Andrew Reynolds
2019-06-27Variable elimination rewrite for quantified strings (#3071)Andrew Reynolds
2019-06-24Stratify unfolding of regular expressions based on polarity (#3067)Andrew Reynolds
2019-06-21Fix and simplify handling of --force-logic (#3062)Andres Noetzli
2019-06-12Refactor parser to define fewer tokens for symbols (#2936)Andres Noetzli
2019-06-11Disable dumping regression for non-dumping builds (#3046)Andres Noetzli
2019-06-11Do not require sygus constructors to be flattened (#3049)Andrew Reynolds
2019-06-10Optimization for negative concatenation membership. (#3048)Andrew Reynolds
2019-06-05Prevent letification from shadowing variables (#3042)Andres Noetzli
2019-06-04Enable proof checking for QF_LRA benchmarks (#2928)Andres Noetzli
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback