summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Expand)Author
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
2018-12-06Enable BV proofs when using an eager bitblaster (#2733)Alex Ozdemir
2018-11-21Quickly recognize when PBE conjectures are infeasible (#2718)Andrew Reynolds
2018-11-21Support string replace all (#2704)Andrew Reynolds
2018-11-07Adding default SyGuS grammar construction for arrays (#2685)Haniel Barbosa
2018-11-07Fix collectEmptyEqs in string rewriter (#2692)Andres Noetzli
2018-11-05Increasing coverage (#2683)yoni206
2018-10-22Recover from wrong use of get-info :reason-unknown (#2667)Andres Noetzli
2018-10-20Disable dumping test for non-dumping builds (#2662)Andres Noetzli
2018-10-18Add OptionException handling during initialization (#2466)Andres Noetzli
2018-10-18Non-implied mode for model cores (#2653)Andrew Reynolds
2018-10-18Non-contributing find replace rewrite (#2652)Andrew Reynolds
2018-10-05Update default options for sygus (#2586)Andrew Reynolds
2018-10-02Allow (_ to_fp ...) in strict parsing mode (#2566)Andres Noetzli
2018-09-30Add rewrite for solving stoi (#2532)Andrew Reynolds
2018-09-26 Fix homogeneous string constant rewrite (#2545)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback