summaryrefslogtreecommitdiff
path: root/test/regress/regress1
AgeCommit message (Expand)Author
2020-07-10Front end support for integer AND (#4717)Andrew Reynolds
2020-07-09Ensure legal elimination for witness rewrite (#4688)Andrew Reynolds
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
2020-07-02Fix regression option (#4680)Andrew Reynolds
2020-06-30Simplify quantifiers strategy for when to apply last call effort check with f...Andrew Reynolds
2020-06-17Do not traverse WITNESS for partial substitutions in extended rewriter (#4630)Andrew Reynolds
2020-06-17Improve polynomial anyterm grammar (#3566)Haniel Barbosa
2020-06-15Fix regressions in regress1 after #4613. (#4616)Aina Niemetz
2020-06-15 Do RE derivation inference only for concrete constant RE (#4609)Andrew Reynolds
2020-06-10(proof-new) Remove arith-snorm option. (#4591)Andrew Reynolds
2020-06-05Smt2 parsing support for nested recursive datatypes (#4575)Andrew Reynolds
2020-06-04Fix abduction with datatypes (#4566)Andrew Reynolds
2020-06-03Do not apply unconstrained simplification when quantifiers are present (#4532)Andrew Reynolds
2020-06-02Do not handle universal quantification on functions in model-based FMF (#4226)Andrew Reynolds
2020-05-22Refactor operator elimination in arithmetic (#4519)Andrew Reynolds
2020-05-21Disable re-elim by default (#4508)Andrew Reynolds
2020-05-19Do not eliminate variables that are equal to unevaluatable terms (#4267)Andrew Reynolds
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
2020-04-30Fix regression (#4424)Andrew Reynolds
2020-04-30Remove skolem share involving pre_first_ctn. (#4423)Andrew Reynolds
2020-04-29Fix strings 2.6 regression (#4413)Andrew Reynolds
2020-04-28Support the SMT-LIB Unicode string standard by default (#4378)Andrew Reynolds
2020-04-25 Fix sets cardinality cycle rule (#4392)Andrew Reynolds
2020-04-22Ensure disequality splits are processed as lemmas (#4380)Andrew Reynolds
2020-04-22Convert V2.5 SMT regressions to V2.6. (#4319)Abdalrhman Mohamed
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-14Disable preregistration of instantiations for cegqi in incremental (#4251)Andrew Reynolds
2020-04-14Remove a few spurious assertions (#4294)Andrew Reynolds
2020-04-12Fixes for extended rewriter (#4278)Andrew Reynolds
2020-04-10Ensure exported sygus solutions match grammar (#4270)Andrew Reynolds
2020-04-08Added CHOOSE operator for sets (#4211)mudathirmahgoub
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2020-03-31Fix fmf benchmark (#4193)Andrew Reynolds
2020-03-31Fix strange bound regression (#4192)Andrew Reynolds
2020-03-30Support indexed operators re.loop and re.^ (#4167)Andrew Reynolds
2020-03-28Change is-cons to (_ is cons) in Sygus benchmarks. (#4174)Abdalrhman Mohamed
2020-03-28Convert the last few Sygus benchmarks to V2. (#4172)Abdalrhman Mohamed
2020-03-27Fix expected output on arith regression (#4162)Andrew Reynolds
2020-03-26Added unit-cube-like test for branch and bound (#3922)Amalee
2020-03-23Simplify auxiliary variable handling in CEGQI (#4141)Andrew Reynolds
2020-03-22Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)Andrew Reynolds
2020-03-21Convert V1 Sygus files to V2. (#4136)Abdalrhman Mohamed
2020-03-20Fix variable shadowing issue in sygus-inference (#4121)Andrew Reynolds
2020-03-20Guard cases of sort inference in quantifier free logics in uf cardinality (#4...Andrew Reynolds
2020-03-20Do not assign higher-order representative if function does not exist (#4073)Andrew Reynolds
2020-03-19Fix regression output related to sygus+bv-div-zero (#4122)Andrew Reynolds
2020-03-13Remove regress for real to int (#4071)Andrew Reynolds
2020-03-12Do not make models for quantified function variables (#4039)Andrew Reynolds
2020-03-11Fix double notify in equality engine (#4036)Andrew Reynolds
2020-03-11Do not enable some SMT-COMP specific options by default (#4038)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback