summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Expand)Author
2020-06-01Merge branch 'master' into issue4367issue4367Andrew Reynolds
2020-06-01Do not parse ->/lambda unless --uf-ho enabled (#4544)Andres Noetzli
2020-06-01fix regressionAndres Noetzli
2020-05-31Set theoryof-mode after theory wideningAndres Noetzli
2020-05-31Do not cache operator eliminations in arith (#4542)Andres Noetzli
2020-05-26Fix an incorrect limit in conversion from real to float (#4418)Martin
2020-05-22Refactor operator elimination in arithmetic (#4519)Andrew Reynolds
2020-05-22(proof-new) Add rewrite corresponding to regular expression inclusion (#4513)Andrew Reynolds
2020-05-20Fix missing check for cardinality one in unconstrained simplifier (#4504)Andrew Reynolds
2020-05-20Normal form equality conflicts and uniqueness check (#4497)Andrew Reynolds
2020-05-20Fix parametric datatype instantiation (#4493)Andrew Reynolds
2020-05-19Do not eliminate variables that are equal to unevaluatable terms (#4267)Andrew Reynolds
2020-05-19Fix cached free variable identifiers in sygus term database (#4394)Andrew Reynolds
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
2020-05-05Always introduce fresh variable for unconstrained APPLY_UF (#4472)Andrew Reynolds
2020-04-28Support the SMT-LIB Unicode string standard by default (#4378)Andrew Reynolds
2020-04-22Convert V2.5 SMT regressions to V2.6. (#4319)Abdalrhman Mohamed
2020-04-22Reinstantiate support for conjunctions in facts (#4377)Andres Noetzli
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-16SyGuS instantiation quantifiers module (#3910)Mathias Preiner
2020-04-15Do not normalize to representatives for variable equalities in conflict-based...Andrew Reynolds
2020-04-14Always assign function values in higher order (#4279)Andrew Reynolds
2020-04-14Fix dump-unsat-cores-full (#4303)Andrew Reynolds
2020-04-13Fix SyGuS define-fun printing from benchmarks coming from v1 parser (#4256)Andrew Reynolds
2020-04-08Perform theory widening eagerly (#4044)Andres Noetzli
2020-04-08Fix dump models and dump proofs (#4230)Andrew Reynolds
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-12New C++ API: Remove support for (reset). (#4037)Aina Niemetz
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback