summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Expand)Author
2020-02-29 Throw warning instead of error for non-constant values in check-model stages...Andrew Reynolds
2020-02-28Add support for str.from_code (#3829)Andres Noetzli
2020-02-28Fix assertion related to assignability in the model. (#3843)Andrew Reynolds
2020-02-28Replace conditional rewrite pass in quantifiers with the extended rewriter (#...Andrew Reynolds
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-26More fixes for printing sygus commands (#3812)Andrew Reynolds
2020-02-26Basic support for regular expression complement (#3437)Andrew Reynolds
2020-02-24bv_to_int preprocessing passyoni206
2020-02-24Make lambda rewriter more robust (#3806)Andres Noetzli
2020-02-21Switch to th_lira.plf (#3741)Alex Ozdemir
2020-02-21Simple changes towards unicode string standard (#3791)Andrew Reynolds
2020-02-20Remove front-end support for Chain (#3767)Andrew Reynolds
2020-02-14Remove quantifiers rewrite rules infrastructure (#3754)Andrew Reynolds
2020-02-08Make "unknown" non-critical for unsat cores check (#3728)Andres Noetzli
2020-02-07Refactor check-model handling in SmtEngine (#3723)Andrew Reynolds
2020-02-06Fix exact sqrt (#3721)Andrew Reynolds
2020-02-03Regression tests for arithmetic proofs. (#3701)Alex Ozdemir
2020-02-03Minor fixes to regressions (#3702)Andrew Reynolds
2020-02-03Fix invariant template inference for trivially infeasible conjecture (#3693)Andrew Reynolds
2020-01-31Fix arithmetic rewriter for exponential (#3688)Andres Noetzli
2020-01-30Ensure literals in FMF decision strategies are in the CNF stream (#3669)Andrew Reynolds
2020-01-30Do not debug check model for models with approximations (#3673)Andrew Reynolds
2020-01-29Fix isLeq function in String utility (#3659)Andrew Reynolds
2020-01-28Avoid PLUS with one child for bv2nat elimination (#3639)Andrew Reynolds
2020-01-22Fix parameteric sorts involving Booleans in sygus default grammars (#3629)Andrew Reynolds
2020-01-10Fix printing of models of uninterpreted sorts (#3597)Andres Noetzli
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback