summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2019-07-23Fix sygus datatype parsing in sygus v1 format (#3113)Andrew Reynolds
2019-07-22Get operators in node (#3094)yoni206
2019-07-19Fixes for sygus with datatypes (#3103)Andrew Reynolds
2019-07-19Fix case of unfolding negative membership in reg exp concatenation (#3101)Andrew Reynolds
2019-07-18Basic rewrites for tolower/toupper (#3095)Andrew Reynolds
2019-07-16Add support for str.tolower and str.toupper (#3092)Andrew Reynolds
2019-07-15 Add string rewrite to distribute character stars over concatenation (#3091)Andrew Reynolds
2019-06-27Variable elimination rewrite for quantified strings (#3071)Andrew Reynolds
2019-06-24Stratify unfolding of regular expressions based on polarity (#3067)Andrew Reynolds
2019-06-24Fix memory leak in unit test (#3068)Andres Noetzli
2019-06-21Fix and simplify handling of --force-logic (#3062)Andres Noetzli
2019-06-21Use TMPDIR environment variable for temp files (#2849)Andres Noetzli
2019-06-12Refactor parser to define fewer tokens for symbols (#2936)Andres Noetzli
2019-06-11Disable dumping regression for non-dumping builds (#3046)Andres Noetzli
2019-06-11Do not require sygus constructors to be flattened (#3049)Andrew Reynolds
2019-06-10Optimization for negative concatenation membership. (#3048)Andrew Reynolds
2019-06-05Prevent letification from shadowing variables (#3042)Andres Noetzli
2019-06-05DRAT-Optimization (#2971)Alex Ozdemir
2019-06-04Enable proof checking for QF_LRA benchmarks (#2928)Andres Noetzli
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
2019-06-01Fix rewriter for regular expression consume (#3029)Andrew Reynolds
2019-05-30Quote symbol when printing empty symbol name (#3025)Andres Noetzli
2019-05-27Avoid substituting Boolean term variables (#3022)Andres Noetzli
2019-05-21Update to symfpu 0.0.7, fixes RTI 3/5 issue (#3007)Martin
2019-05-18FP: Fix regression test and enable SymFPU on Travis. (#3013)Aina Niemetz
2019-05-17Fix BV ITE rewrite (#3004)Andres Noetzli
2019-05-17Add the problematic input from issue 2183 as a regression test (#3008)Martin
2019-05-15Fix model of Boolean vars with eager bit-blaster (#2998)Andres Noetzli
2019-05-15Fix printing of bvurem (#2963)Andrew Reynolds
2019-05-09Fixes for relational triggers (#2967)Andrew Reynolds
2019-05-06Add support for re.all (#2980)Andres Noetzli
2019-05-01Fix re-elim-agg regressions (#2987)Andrew Reynolds
2019-05-01 Use total versions of div/mod in re-elim-agg (#2986)Andrew Reynolds
2019-04-30Fix concat-find regexp elimination (#2983)Andres Noetzli
2019-04-30Remove stoi solve rewrite (#2985)Andrew Reynolds
2019-04-29Eliminate APPLY kind (#2976)Andrew Reynolds
2019-04-25New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)Aina Niemetz
2019-04-17Fix extended function decomposition (#2960)Andrew Reynolds
2019-04-16Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)Andres Noetzli
2019-04-16Stratify enumerative instantiation (#2954)Andrew Reynolds
2019-04-16Minor simplifications to theory quantifiers (#2953)Andrew Reynolds
2019-04-11 Eliminate Boolean ITE within terms, fixes 2947 (#2949)Andrew Reynolds
2019-04-05Fix another corner case of datatypes+PBE (#2938)Andrew Reynolds
2019-04-05fix fp issue (#2940)Haniel Barbosa
2019-04-04Ignoring FP benchmarks with "unsafe" sizes unless option (#2931)Haniel Barbosa
2019-04-03Update copyright headers.Aina Niemetz
2019-04-03Fix combination of datatypes + strings in PBE (#2930)Andrew Reynolds
2019-04-01FP: Fix wrong model due to partial assignment (#2910)Andres Noetzli
2019-04-01Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)Andres Noetzli
2019-04-01Move slow string regression to regress3 (#2913)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback