summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers
AgeCommit message (Expand)Author
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
2018-08-20Add regressions that increase coverage (#2337)Andrew Reynolds
2018-08-02Improve CEGQI heuristics involving equality and multiple instantiations (#2254)Andrew Reynolds
2018-08-01Improvements and fixes in cegqi arithmetic (#2247)Andrew Reynolds
2018-07-24Improvements to sets + cardinality + quantifiers (#2200)Andrew Reynolds
2018-06-15Disable solving non-linear BV literals by default (#2070)Andrew Reynolds
2018-06-04Enable cegqi (with model values) for floating point by default (#2023)Andrew Reynolds
2018-06-01Apply preprocessing to counterexample lemmas in CEGQI (#2027)Andrew Reynolds
2018-05-25Reenable repair const (#1983)Andrew Reynolds
2018-05-22Make sygus infer find function definitions (#1951)Andrew Reynolds
2018-05-03Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)Andrew Reynolds
2018-04-25Add benchmark requiring subgoal generation with induction. Disable option. (#...Andrew Reynolds
2018-04-16Disable check proofs/unsat cores for two regs (#1785)Andres Noetzli
2018-04-06Add define rec fun to cvc parser (#1738)Arjun Viswanathan
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback