summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-21fixstratRe-062019_expAndres Noetzli
2019-06-21different heuristicAndres Noetzli
2019-06-20Stratify unfolding of regular expressions based on polarityajreynol
2019-06-18 Strings: More aggressive skolem normalization (#2761)Andres Noetzli
2019-06-15Use Ubuntu 16.04 on Travis (#3059)Andres Noetzli
2019-06-13Add lemma for the range of values of str.indexof (#3054)Andres Noetzli
2019-06-13 Shorten explanation for strings inference I_Norm_S (#3051)Andrew Reynolds
2019-06-12Fix warning (#3053)Haniel Barbosa
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-11Fix compilation issue for Java bindings + CLN (#3045)Andres Noetzli
2019-06-11NA Tangent reverse implication (#3050)Ahmed Irfan
2019-06-11 Minor cleaning of conflict-based instantiation (#2966)Andrew Reynolds
2019-06-11Do not require sygus constructors to be flattened (#3049)Andrew Reynolds
2019-06-11 Fix spurious assertion in get-value (#3052)Andrew Reynolds
2019-06-10Optimization for negative concatenation membership. (#3048)Andrew Reynolds
2019-06-10Optimization for strings normalize disequalities (#3047)Andrew Reynolds
2019-06-05Prevent letification from shadowing variables (#3042)Andres Noetzli
2019-06-05DRAT-Optimization (#2971)Alex Ozdemir
2019-06-05Add support for SWIG 4 (#3041)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-06-03[SMT-COMP] No unconstrained simp for QF_LIA UC (#3039)Andres Noetzli
2019-06-02[SMT-COMP] Increase sequential portfolio times (#3038)Andres Noetzli
2019-06-02[SMT-COMP 2019] Use lazy BV as backup for QF_UFBV (#3037)Andres Noetzli
2019-06-02Enable SymFPU assertions in production (#3036)Andres Noetzli
2019-06-02[SMT-COMP 2019] Update run script for unsat cores (#3034)Andres Noetzli
2019-06-02Add check for limit of number of node children (#3035)Andres Noetzli
2019-06-01Update QF_BV options for SMT-COMP 2019. (#3033)Aina Niemetz
2019-06-01 Require that FMF model basis terms are variables (#3031)Andrew Reynolds
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-20[SMT-COMP 2019] Update run scripts to match tracks (#3018)Andres Noetzli
2019-05-18FP: Fix regression test and enable SymFPU on Travis. (#3013)Aina Niemetz
2019-05-17Update QF_NIA strategy (#3012)Andrew Reynolds
2019-05-17[SMT-COMP2019] Better strings configuration (#3010)Andres Noetzli
2019-05-17Support for incremental bit-blasting with CaDiCaL (#3006)Andres Noetzli
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 iterators in Java API (#3000)Andres Noetzli
2019-05-15cmake: Install JAR and JNI files for Java bindings. (#3002)Mathias Preiner
2019-05-15 BV: Do not enable abstraction when eager bit-blasting by default. (#3001)Aina Niemetz
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-10Disable relational triggers (#2994)Andrew Reynolds
2019-05-09Fixes for relational triggers (#2967)Andrew Reynolds
2019-05-06Add support for re.all (#2980)Andres Noetzli
2019-05-02Simple optimizations to core strings theory. (#2988)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback