summaryrefslogtreecommitdiff
path: root/test/regress/regress1
AgeCommit message (Expand)Author
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
2020-03-11Guard against null relevancy condition in SyGuS (#4033)Andrew Reynolds
2020-03-11Remove experimental symmetry breaker (#4005)Andrew Reynolds
2020-03-11Fix non-parametrized operators in subgoal generation (#4023)Andrew Reynolds
2020-03-11Fix duplicate variable issue in sygus-qe-preproc (#4013)Andrew Reynolds
2020-03-10Fix options for regression: --sort-inference is incompatible with unsat cores...Andrew Reynolds
2020-03-10Fix assertion failure in sort inference for Boolean equalities (#3993)Andrew Reynolds
2020-03-10Do not set values for non-linear mult terms in collectModelInfo (#3983)Andrew Reynolds
2020-03-10Do not traverse quantifiers in nl ext purify (#3982)Andrew Reynolds
2020-03-09Rename sygus option name (#3977)Andrew Reynolds
2020-03-09Remove instantiation propagator infrastructure (#3975)Andrew Reynolds
2020-03-09Ensure standard miniscoping is applied before aggressive miniscoping (#3974)Andrew Reynolds
2020-03-09Fix type issue in arith rewrite equality (#3972)Andrew Reynolds
2020-03-08Rewrite again full for DIV rewrite (#3945)Andrew Reynolds
2020-03-06Remove tester name from APIs (#3929)Andrew Reynolds
2020-03-06Ignore model check warning in regression test (#3926)Andres Noetzli
2020-03-06Support default sygus grammar construction for sets (#3842)Andrew Reynolds
2020-03-05Fix issues with real to int (#3918)Andrew Reynolds
2020-02-28Replace conditional rewrite pass in quantifiers with the extended rewriter (#...Andrew Reynolds
2020-02-26Use side effect utility for non-linear lemmas (#3780)Andrew Reynolds
2020-02-26Fix regression (#3827)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback