summaryrefslogtreecommitdiff
path: root/test/regress/regress1
AgeCommit message (Expand)Author
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
2020-02-11Fix term simplification based on entailment in quantifiers rewriter (#3746)Andrew Reynolds
2020-02-08Fix rewrite rules sat regressions (#3734)Andrew Reynolds
2020-02-07Univeset Cardinality constraints for infinite types (#3712)mudathirmahgoub
2020-02-07Refactor check-model handling in SmtEngine (#3723)Andrew Reynolds
2020-02-03Minor fixes to regressions (#3702)Andrew Reynolds
2020-02-03Fix cardinality of uninterpreted types when univset is not used (#3663)mudathirmahgoub
2020-02-03Split on model values when repaired model from non-linear is inconsisent (#3668)Andrew Reynolds
2020-02-03Fix corner case of empty domains in bounded fmf (#3690)Andrew Reynolds
2020-01-31Refactor relevance vectors for asserted quantifiers (#3666)Andrew Reynolds
2020-01-30Fix rep set increment for empty domains (#3682)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback