summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers
AgeCommit message (Expand)Author
2020-09-14Fix needsModel method for CEGQI (#5048)Andrew Reynolds
2020-09-01[API] Fix Python Examples (#4943)Andres Noetzli
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-08-19Require `--strings-exp` when using `str.substr` (#4916)Andres Noetzli
2020-08-19[Regressions] Do not test `--check-proofs` anymore (#4914)Andres Noetzli
2020-08-11Fix unsupported option in regress1. (#4874)Andrew Reynolds
2020-07-14Fix regression output. (#4741)Andrew Reynolds
2020-07-13Debug instantiations output (#4739)Andrew Reynolds
2020-07-13Statistics on instantiations per quantified formula. (#4719)Andrew Reynolds
2020-07-09Ensure legal elimination for witness rewrite (#4688)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-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-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2020-03-23Simplify auxiliary variable handling in CEGQI (#4141)Andrew Reynolds
2020-03-13Remove regress for real to int (#4071)Andrew Reynolds
2020-03-11Fix non-parametrized operators in subgoal generation (#4023)Andrew Reynolds
2020-03-09Remove instantiation propagator infrastructure (#3975)Andrew Reynolds
2020-03-06Ignore model check warning in regression test (#3926)Andres Noetzli
2020-03-05Fix issues with real to int (#3918)Andrew Reynolds
2020-02-19Delay enumerative instantiation if theory engine does not need check (#3774)Andrew Reynolds
2020-02-17Option to limit the number of rounds of enumerative instantiation (#3760)Andrew Reynolds
2020-02-17 Fix soundness bug in reduction of integer div/mod (#3766)Andrew Reynolds
2020-02-11Fix term simplification based on entailment in quantifiers rewriter (#3746)Andrew Reynolds
2020-01-31Refactor relevance vectors for asserted quantifiers (#3666)Andrew Reynolds
2020-01-30Weaken assertion for models with approximations (#3667)Andrew Reynolds
2020-01-04Fix finiteness check for bounded fmf (#3589)Andrew Reynolds
2019-12-10Allow unsat cores with sygus inference (#3550)Andrew Reynolds
2019-12-09Fix case of uninterpreted constant instantiation in FMF (#3543)Andrew Reynolds
2019-12-05Refactor mode options for Unif+PI (#3531)Andrew Reynolds
2019-12-02 Update ownership policy for dynamic quantifiers splitting (#3493)Andrew Reynolds
2019-11-01Fix non-termination in datatype type enumerator (#3369)Andrew Reynolds
2019-10-08Limit cases of sygus inference based on type (#3370)Andrew Reynolds
2019-10-08Fix method for getting arithmetic function definition body (#3371)Andrew Reynolds
2019-09-16Remove equality inference option for quantifiers (#3282)Andrew Reynolds
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
2019-08-23Update dynamic splitting strategy for quantifiers (#3162)Andrew Reynolds
2019-06-27Variable elimination rewrite for quantified strings (#3071)Andrew Reynolds
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
2019-05-09Fixes for relational triggers (#2967)Andrew Reynolds
2018-11-19Fix E-matching for case where candidate generator is not properly initialized...Andrew Reynolds
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-24 Remove spurious disabling of cbqi-all (#2368)Andrew Reynolds
2018-08-23Fix regression requiring proof build. (#2364)Andrew Reynolds
2018-08-22More regressions that increase coverage (#2354)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback