summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2019-10-08Disallow --proof and --incremental (#3332)Andres Noetzli
2019-10-08Make ackermannization generally applicable rather than just BV (#3315)Ying Sheng
2019-10-07New C++ API: Add Term::getId(). (#3360)Aina Niemetz
2019-10-06Fix typo in regression (#3359)Andrew Reynolds
2019-10-06Fix str to int reduction (#3358)Andrew Reynolds
2019-10-03Disable proofs for unsupported logics (#3327)yoni206
2019-09-30Trivial solve method for single invocation sygus (#3328)Andrew Reynolds
2019-09-29Add rewrite for splitting equalities (#2957)Andres Noetzli
2019-09-29Avoid cases of empty sygus grammars (#3301)Andrew Reynolds
2019-09-29Fail single invocation techniques when utility inference fails. (#3322)Andrew Reynolds
2019-09-27Support smt2 language "match" term (#3258)Andrew Reynolds
2019-09-27Fix case of disjunctive conclusion in strings (#3254)Andrew Reynolds
2019-09-26CVC print support for recoverable failure (#3323)Andrew Reynolds
2019-09-25 Fix off by one error in strings flat form explanation (#3273)Andrew Reynolds
2019-09-25Add isParameterized function to Expr (#3303)Andrew Reynolds
2019-09-25Use separate CMake project for CVC4 examples. (#3196)Mathias Preiner
2019-09-24Return choice functions for approximate values in get-value (#3304)Andrew Reynolds
2019-09-19Support context-(in)dependent decision strategies. (#3281)Andrew Reynolds
2019-09-18Add support for creating constant arrays to the new C++ API (#3296)makaimann
2019-09-18Decouple fmf-bound and finite-model-find (#3297)Andrew Reynolds
2019-09-16Avoid computing cardinality when constructing models (#3268)Andrew Reynolds
2019-09-16Fix spurious meta-info in regression (#3294)Andrew Reynolds
2019-09-16Remove equality inference option for quantifiers (#3282)Andrew Reynolds
2019-09-16 Fix HO model construction for functions having Boolean arguments (#3158)Andrew Reynolds
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-19New C++ API: Add checks for Solver::checkValid and Solver::checkValidAssuming...Aina Niemetz
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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback