summaryrefslogtreecommitdiff
path: root/test/regress/regress1
AgeCommit message (Expand)Author
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
2020-02-26More fixes for printing sygus commands (#3812)Andrew Reynolds
2020-02-26Basic support for regular expression complement (#3437)Andrew Reynolds
2020-02-26Use default consts when not using any const during grammar normalization (#3807)Andrew Reynolds
2020-02-26Fix node arity issue in reduction of int2bv (#3777)Andrew Reynolds
2020-02-26Support for witnessing choice in models (#3781)Andrew Reynolds
2020-02-21Switch to th_lira.plf (#3741)Alex Ozdemir
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-14Remove quantifiers rewrite rules infrastructure (#3754)Andrew Reynolds
2020-02-12Ensure ext rewrites for associative ops dont throw assertions for kind aritie...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback