summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2020-01-15New C++ API: Add nullary constructor for Result. (#3603)Aina Niemetz
2020-01-14Generalize example-based sym breaking to conjectures with constant function a...Andrew Reynolds
2020-01-14Disable unsat cores for regression that times out (#3607)Andres Noetzli
2020-01-10Fix side condition check in sygus core connective (#3600)Andrew Reynolds
2020-01-10Fix printing of models of uninterpreted sorts (#3597)Andres Noetzli
2020-01-10Track trivial cases in transition inference (#3598)Andrew Reynolds
2020-01-08Fix backtracking issue in sygus fast enumerator (#3593)Andrew Reynolds
2020-01-07Universe set cardinality for finite types with finite cardinality (#3392)mudathirmahgoub
2020-01-07Update any-constant and normalization policies for sygus grammars (#3583)Andrew Reynolds
2020-01-04Fix finiteness check for bounded fmf (#3589)Andrew Reynolds
2019-12-30[proof] ITE translation fix (#3484)Alex Ozdemir
2019-12-23Initial support for string reverse (#3581)Andrew Reynolds
2019-12-18Increment Taylor degree for tangent and secant plane inferences for transcend...Andrew Reynolds
2019-12-18Avoid calling rewriter from type checker (#3548)Andres Noetzli
2019-12-17Fix spurious parse error for rational real array constants (#3554)Andrew Reynolds
2019-12-16Support ackermannization on uninterpreted sorts in BV (#3372)Ying Sheng
2019-12-13Add support for set comprehension (#3312)Andrew Reynolds
2019-12-13Disable check-synth-sol in regression with recursive functions (#3560)Andrew Reynolds
2019-12-12Make CEGIS sampling robust to non-vanilla CEGIS (#3559)Andrew Reynolds
2019-12-12Fix Unif+PI algorithm with symbolic unfolding (#3558)Haniel Barbosa
2019-12-12Fixes for regressions (#3557)Andrew Reynolds
2019-12-11Fix CEGIS refinement for recursive functions evaluation (#3555)Andrew Reynolds
2019-12-11Do not substitute beneath arithmetic terms in the non-linear solver (#3324)Andrew Reynolds
2019-12-10Fix ufho issues (#3551)Haniel Barbosa
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-08[Regressions] Require proof support for abduction (#3546)Andres Noetzli
2019-12-06Simplify rewrite for character matching (#3545)Andres Noetzli
2019-12-06New algorithm for interpolation and abduction based on unsat cores (#3255)Andrew Reynolds
2019-12-06Add ExprManager as argument to Datatype (#3535)Andrew Reynolds
2019-12-06[proof] Eliminate side-condition from ER signature (#3230)Alex Ozdemir
2019-12-05Make nonlinear solver intercept model assignments from the linear arithmetic ...Andrew Reynolds
2019-12-05Refactor mode options for Unif+PI (#3531)Andrew Reynolds
2019-12-05Bi-directional unrolling of R* regular expressions (#3532)Andres Noetzli
2019-12-04Add mkOp for a single Kind (#3522)makaimann
2019-12-04Fix the subtyping relation for functions (#3494)Andrew Reynolds
2019-12-04New grammar construction modes for SyGuS (#3486)Andrew Reynolds
2019-12-04Fix (#3530)Andrew Reynolds
2019-12-04Fix single invocation solution construction for multiple function case (#3516)Andrew Reynolds
2019-12-03Rewrite `str.contains` used for character matching (#3519)Andres Noetzli
2019-12-02Minor refactor: rename opterm_black to op_black (#3521)makaimann
2019-12-02[SMT2 Printer] Quote symbols starting with digit (#3517)Andres Noetzli
2019-12-02OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ AP...makaimann
2019-12-02 Update ownership policy for dynamic quantifiers splitting (#3493)Andrew Reynolds
2019-12-02Fix case of higher-order + sygus inference (#3509)Andrew Reynolds
2019-12-01Ensure quantifiers options are set with --no-strings-lazy-pp (#3515)Andrew Reynolds
2019-12-01Prevent ref count from reaching zero in BV instantiator (#3512)Andres Noetzli
2019-11-29Competition build: Skip parsing error regression (#3511)Andres Noetzli
2019-11-29Fix fast SyGuS enumeration for interpreted constants (#3501)Andrew Reynolds
2019-11-27Fix sygus inference for choice functions introduced at preprocess (#3500)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback