summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Expand)Author
2019-12-30[proof] ITE translation fix (#3484)Alex Ozdemir
2019-12-23Initial support for string reverse (#3581)Andrew Reynolds
2019-12-18Avoid calling rewriter from type checker (#3548)Andres Noetzli
2019-12-17Fix spurious parse error for rational real array constants (#3554)Andrew Reynolds
2019-12-16Support ackermannization on uninterpreted sorts in BV (#3372)Ying Sheng
2019-12-13Add support for set comprehension (#3312)Andrew Reynolds
2019-12-10Fix ufho issues (#3551)Haniel Barbosa
2019-12-05Make nonlinear solver intercept model assignments from the linear arithmetic ...Andrew Reynolds
2019-12-05Refactor mode options for Unif+PI (#3531)Andrew Reynolds
2019-12-05Bi-directional unrolling of R* regular expressions (#3532)Andres Noetzli
2019-12-04Fix the subtyping relation for functions (#3494)Andrew Reynolds
2019-12-02[SMT2 Printer] Quote symbols starting with digit (#3517)Andres Noetzli
2019-12-01Ensure quantifiers options are set with --no-strings-lazy-pp (#3515)Andrew Reynolds
2019-11-29Competition build: Skip parsing error regression (#3511)Andres Noetzli
2019-11-27 Fix indexof range lemma (#3499)Andrew Reynolds
2019-11-25Better front-end type checking for SyGuS (#3496)Andrew Reynolds
2019-11-18Fix reduction of `sqrt` (#3478)Andres Noetzli
2019-11-13Allow (set-logic ...) after (reset) (#3457)Andres Noetzli
2019-11-04Avoid non-well-founded sygus grammars (#3434)Andrew Reynolds
2019-10-28Fix for non-linear models (#3410)Andrew Reynolds
2019-10-28Fix integer division rewrite (#3415)Andres Noetzli
2019-10-27Fix global-declarations support (#3403)Andres Noetzli
2019-10-15Fix regression (#3393)Andres Noetzli
2019-10-14Disable regression test for competition build (#3388)Andres Noetzli
2019-10-13Eliminate negative constant coefficients in div/mod (#2929)Andrew Reynolds
2019-10-11Check that logic is set when synth-fun command is encountered (#3384)Andrew Reynolds
2019-10-08Avoid printing success for `--force-logic` (#3363)Andres Noetzli
2019-10-08Limit cases of sygus inference based on type (#3370)Andrew Reynolds
2019-10-08[CVC Parser] Add support for regular expressions (#3346)Andres Noetzli
2019-10-08Disallow --proof and --incremental (#3332)Andres Noetzli
2019-10-08Make ackermannization generally applicable rather than just BV (#3315)Ying Sheng
2019-10-03Disable proofs for unsupported logics (#3327)yoni206
2019-09-30Trivial solve method for single invocation sygus (#3328)Andrew Reynolds
2019-09-26CVC print support for recoverable failure (#3323)Andrew Reynolds
2019-09-24Return choice functions for approximate values in get-value (#3304)Andrew Reynolds
2019-09-18Decouple fmf-bound and finite-model-find (#3297)Andrew Reynolds
2019-09-13Disallow let in sygus grammars, check for free variables in sygus constructor...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-13Properly implement logic info for separation logic (#3176)Andrew Reynolds
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-01Enable sygus logic when produce-abducts is true (#3144)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-30Remove hard coded option for TPTP regressions in run_regression (#3128)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback