summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2019-08-13New C++ API: Add checks and tests for Solver::simplify. (#3170)Aina Niemetz
2019-08-13New C++ API: Fix test names of solver_black unit test. (#3170)Aina Niemetz
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-11New C++ API: Add templated getIndices method for OpTerm (#3073)makaimann
2019-08-08Fix issues with Ninja build system and add configure option. (#3166)Mathias Preiner
2019-08-07New C++ API: Add checks and tests for push/pop. (#3121)Aina Niemetz
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-01Fix BVGauss unit tests. (#3142)Mathias Preiner
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-31adding bv_gauss unit test to build files (#3135)yoni206
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-22Get operators in node (#3094)yoni206
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-24Fix memory leak in unit test (#3068)Andres Noetzli
2019-06-21Fix and simplify handling of --force-logic (#3062)Andres Noetzli
2019-06-21Use TMPDIR environment variable for temp files (#2849)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-05DRAT-Optimization (#2971)Alex Ozdemir
2019-06-04Enable proof checking for QF_LRA benchmarks (#2928)Andres Noetzli
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
2019-06-01Fix rewriter for regular expression consume (#3029)Andrew Reynolds
2019-05-30Quote symbol when printing empty symbol name (#3025)Andres Noetzli
2019-05-27Avoid substituting Boolean term variables (#3022)Andres Noetzli
2019-05-21Update to symfpu 0.0.7, fixes RTI 3/5 issue (#3007)Martin
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback