summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2020-03-03Refactoring and cleaning the type enumerator for sets (#3908)mudathirmahgoub
2020-02-29 Throw warning instead of error for non-constant values in check-model stages...Andrew Reynolds
2020-02-28Add support for str.from_code (#3829)Andres Noetzli
2020-02-28Fix assertion related to assignability in the model. (#3843)Andrew Reynolds
2020-02-28Replace conditional rewrite pass in quantifiers with the extended rewriter (#...Andrew Reynolds
2020-02-27Fix large models for strings (#3835)Andrew Reynolds
2020-02-26Add support for is_digit and regular expression difference (#3828)Andrew Reynolds
2020-02-26Disable regression that times out on debug (#3833)Andrew Reynolds
2020-02-26Use side effect utility for non-linear lemmas (#3780)Andrew Reynolds
2020-02-26Fix regression (#3827)Andrew Reynolds
2020-02-26More fixes for printing sygus commands (#3812)Andrew Reynolds
2020-02-26Basic support for regular expression complement (#3437)Andrew Reynolds
2020-02-26Use default consts when not using any const during grammar normalization (#3807)Andrew Reynolds
2020-02-26Fix node arity issue in reduction of int2bv (#3777)Andrew Reynolds
2020-02-26Support for witnessing choice in models (#3781)Andrew Reynolds
2020-02-26Remove portfolio leftovers (#3821)Andres Noetzli
2020-02-24bv_to_int preprocessing passyoni206
2020-02-24Utilities for words (#3797)Andrew Reynolds
2020-02-24Convert parser input interface to api::Term (#3809)Andrew Reynolds
2020-02-24Add missing functions to new C++ API (#3769)Andrew Reynolds
2020-02-24Make lambda rewriter more robust (#3806)Andres Noetzli
2020-02-21Switch to th_lira.plf (#3741)Alex Ozdemir
2020-02-21New C++ API: Remove TOTAL kinds. (#3794)Aina Niemetz
2020-02-21Simple changes towards unicode string standard (#3791)Andrew Reynolds
2020-02-20Remove front-end support for Chain (#3767)Andrew Reynolds
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
2020-02-19Add Python bindings using Cython -- see below for more details (#2879)makaimann
2020-02-19Delay enumerative instantiation if theory engine does not need check (#3774)Andrew Reynolds
2020-02-19Change Record to shared_ptr (#3778)Andrew Reynolds
2020-02-18Change datatype selector/constructor/tester to terms (#3773)makaimann
2020-02-17Option to limit the number of rounds of enumerative instantiation (#3760)Andrew Reynolds
2020-02-17 Fix soundness bug in reduction of integer div/mod (#3766)Andrew Reynolds
2020-02-15Disable regression (#3761)Andrew Reynolds
2020-02-14Remove quantifiers rewrite rules infrastructure (#3754)Andrew Reynolds
2020-02-12Ensure ext rewrites for associative ops dont throw assertions for kind aritie...Andrew Reynolds
2020-02-11run_regression: Distinguish between timeout and failure. (#3750)Mathias Preiner
2020-02-11Fix term simplification based on entailment in quantifiers rewriter (#3746)Andrew Reynolds
2020-02-08Fix rewrite rules sat regressions (#3734)Andrew Reynolds
2020-02-08Make "unknown" non-critical for unsat cores check (#3728)Andres Noetzli
2020-02-07Univeset Cardinality constraints for infinite types (#3712)mudathirmahgoub
2020-02-07Refactor check-model handling in SmtEngine (#3723)Andrew Reynolds
2020-02-06Fix exact sqrt (#3721)Andrew Reynolds
2020-02-03Regression tests for arithmetic proofs. (#3701)Alex Ozdemir
2020-02-03Increase regression test time limit to 1200s. (#3704)Aina Niemetz
2020-02-03Minor fixes to regressions (#3702)Andrew Reynolds
2020-02-03Fix cardinality of uninterpreted types when univset is not used (#3663)mudathirmahgoub
2020-02-03Split on model values when repaired model from non-linear is inconsisent (#3668)Andrew Reynolds
2020-02-03Fix invariant template inference for trivially infeasible conjecture (#3693)Andrew Reynolds
2020-02-03Fix corner case of empty domains in bounded fmf (#3690)Andrew Reynolds
2020-02-03Example inference utility (#3670)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback