summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
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
2019-03-29Apply empty splits more aggressively in sets+cardinality (#2907)Andrew Reynolds
2019-03-28Fix freeing nodes with maxed refcounts (#2903)Andres Noetzli
2019-03-28Fix issues in cvc parser (#2901)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2019-03-23BV: Fix typerules for rotate operators. (#2895)Aina Niemetz
2019-03-23Fix memory leak when using subsolvers (#2893)Andres Noetzli
2019-03-23Strip non-matching beginning from indexof operator (#2885)Andres Noetzli
2019-03-22More fixes for PBE with datatypes (#2882)Andrew Reynolds
2019-03-22Fix stripConstantEndpoints in strings rewriter (#2883)Andres Noetzli
2019-03-21Rewrite selectors correctly applied to constructors (#2875)Andrew Reynolds
2019-03-19Sygus abduction feature (#2744)Andrew Reynolds
2019-03-19Fix fairness issue with fast sygus enumerator (#2873)Andrew Reynolds
2019-03-18New C++: Remove redundant mkBoundVar function.Aina Niemetz
2019-03-18New C++: Remove redundant mkVar function.Aina Niemetz
2019-03-18BitVector: Allow base 10 in constructor. (#2870)Aina Niemetz
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-02-28ErProof class with LFSC output (#2812)Alex Ozdemir
2019-02-13New C++ API: Remove redundant declareFun function. (#2837)Aina Niemetz
2019-02-13Rewrite simple regexp pattern to str.contains (#2827)Andres Noetzli
2019-02-12New C++ API: Remove redundant mkTerm function. (#2836)Aina Niemetz
2019-02-11New C++ API: Unit tests for declare* functions. (#2831)Aina Niemetz
2019-02-05Make stripConstantEndpoints() less aggressive (#2830)Andres Noetzli
2019-02-03Add rewrite for contains + const strings replace (#2828)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback