summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Expand)Author
2020-04-08Merge branch 'master' into fix3991fix3991Andrew Reynolds
2020-04-08Fix dump models and dump proofs (#4230)Andrew Reynolds
2020-04-07mergeAndres Noetzli
2020-03-31Support char smt-lib syntax (#4188)Andrew Reynolds
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2020-03-30Support indexed operators re.loop and re.^ (#4167)Andrew Reynolds
2020-03-30Frontend support for the choice operator (#4175)mudathirmahgoub
2020-03-28Convert the last few Sygus benchmarks to V2. (#4172)Abdalrhman Mohamed
2020-03-27Fix issues with unsat cores and reset-assertions (#4159)Andres Noetzli
2020-03-27Support unicode internal representation and escape sequences (#3852)Andrew Reynolds
2020-03-26Added unit-cube-like test for branch and bound (#3922)Amalee
2020-03-24Int2BV fail on demand (#4079)yoni206
2020-03-21Convert V1 Sygus files to V2. (#4136)Abdalrhman Mohamed
2020-03-20Don't run bv_nat parse test with competition build (#4126)Andres Noetzli
2020-03-19Only apply testConstStringInRegExp to const regexp (#4120)Andres Noetzli
2020-03-18Only allow bv2nat/int2bv with BV and integer logic (#4118)Andres Noetzli
2020-03-18Fix issue with multiple infinities in CEGQI for LIRA (#4114)Andrew Reynolds
2020-03-16Create master equality engine at context level 0 (#4081)Andres Noetzli
2020-03-12Do not allow quantifiers over real variables in real to int pass. (#4049)Andrew Reynolds
2020-03-12Add additional regressionAndres Noetzli
2020-03-12Eagerly expand definitionsAndres Noetzli
2020-03-12New C++ API: Remove support for (reset). (#4037)Aina Niemetz
2020-03-12Misisng unit testAndres Noetzli
2020-03-11reset-assertions: Update TheoryEngine's PropEngine* (#4032)Andres Noetzli
2020-03-10Set assertion in `CnfStream::ensureLiteral()` (#3927)Andres Noetzli
2020-03-10Fix real to int for parameterized kinds (#4016)Andrew Reynolds
2020-03-10Fix sort inference for top-level Boolean variables (#4012)Andrew Reynolds
2020-03-10Fix issue with reset-assertions. (#3988)Aina Niemetz
2020-03-10 Fix real as int for incremental (#3979)Andrew Reynolds
2020-03-09Enhancement: make the bool-to-bv pass more robust and targeted (#3021)makaimann
2020-03-09Make registration of unit clauses more robust (#3965)Andres Noetzli
2020-03-07Explicit end marker for models printed in the CVC language (#3934)Ying Sheng
2020-03-06Remove tester name from APIs (#3929)Andrew Reynolds
2020-03-06Support default sygus grammar construction for sets (#3842)Andrew Reynolds
2020-03-05Remove --apply-to-const preprocessing pass (#3919)Andres Noetzli
2020-03-05Fix issues with real to int (#3918)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback