summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Expand)Author
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
2019-09-04Remove duplicate regression tests. (#3227)Mathias Preiner
2019-08-29Better heuristic for str.code/re.range (#3220)Andres Noetzli
2019-08-29Infer conflicts based on regular expression inclusion (#3234)Andres Noetzli
2019-08-13Properly implement logic info for separation logic (#3176)Andrew Reynolds
2019-08-06Properly parse qualified identifiers (#3111)Andrew Reynolds
2019-08-04Fix regression script for incremental SMT-LIB v2 benchmarks. (#3155)Mathias Preiner
2019-08-02Update CaDiCaL to version 1.0.3. (#3137)Mathias Preiner
2019-08-01Enable sygus logic when produce-abducts is true (#3144)Andrew Reynolds
2019-07-31Parsing THF and adding several regressions (#3131)Haniel Barbosa
2019-07-30Minor improvement for rewriter for str.replace (#3124)Andrew Reynolds
2019-07-30Remove hard coded option for TPTP regressions in run_regression (#3128)Haniel Barbosa
2019-07-23Fix sygus datatype parsing in sygus v1 format (#3113)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-06-21Fix and simplify handling of --force-logic (#3062)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-05Prevent letification from shadowing variables (#3042)Andres Noetzli
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-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-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-06Add support for re.all (#2980)Andres Noetzli
2019-04-30Remove stoi solve rewrite (#2985)Andrew Reynolds
2019-04-29Eliminate APPLY kind (#2976)Andrew Reynolds
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-16Minor simplifications to theory quantifiers (#2953)Andrew Reynolds
2019-04-11 Eliminate Boolean ITE within terms, fixes 2947 (#2949)Andrew Reynolds
2019-04-04Ignoring FP benchmarks with "unsafe" sizes unless option (#2931)Haniel Barbosa
2019-04-01FP: Fix wrong model due to partial assignment (#2910)Andres Noetzli
2019-03-28Fix issues in cvc parser (#2901)Andrew Reynolds
2019-03-16Enable CryptoMiniSat-backed BV proofs (#2847)Alex Ozdemir
2019-03-15New beta-reduction for HOL solving (#2869)Haniel Barbosa
2019-03-14Use zero slope tangent planes for transcendental functions (#2803)Andrew Reynolds
2019-03-14Implement proper semantics for TPTP predicate is_rat. (#2861)Andrew Reynolds
2019-03-12 Move tuple/record update elimination from ppRewrite to expandDefinition (#2839)Andrew Reynolds
2019-01-22 Fix tuple and record CVC printing (#2818)Andrew Reynolds
2019-01-22 Fix parsing of overloaded parametric datatype selectors (#2819)Andrew Reynolds
2019-01-16Add option to print BV constants in binary (#2805)Andres Noetzli
2019-01-15Fix constant contains ITOS rewrite (#2799)Andrew Reynolds
2019-01-15 Fix unsound double abs rewrite rule for FP (#2792)Andrew Reynolds
2018-12-14 Fix extended rewriter for binary associative operators. (#2751)Andrew Reynolds
2018-12-11Remove alternate versions of mbqi (#2742)Andrew Reynolds
2018-12-10BoolToBV modes (off, ite, all) (#2530)makaimann
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback