summaryrefslogtreecommitdiff
path: root/test/regress/regress0/parser
AgeCommit message (Expand)Author
2021-06-16Make symfpu a required dependency. (#6749)Aina Niemetz
2021-05-19Improve handling of `:named` attributes (#6549)Andres Noetzli
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2021-01-26Reestablishing support for define-sort (#5810)Haniel Barbosa
2021-01-21Add div, mod, abs in non-strict parsing mode (#5793)Andrew Reynolds
2021-01-20SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)Aina Niemetz
2020-12-17Simplify and fix check models (#5685)Andrew Reynolds
2020-11-12Models standard (#5415)yoni206
2020-10-08reset-assertions: Remove all non-global symbols in the parser (#5229)Andres Noetzli
2020-09-25Restrict bvxnor to only allow two operands (was n-ary). (#5138)Aina Niemetz
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
2020-03-30Frontend support for the choice operator (#4175)mudathirmahgoub
2020-03-20Don't run bv_nat parse test with competition build (#4126)Andres Noetzli
2020-03-18Only allow bv2nat/int2bv with BV and integer logic (#4118)Andres Noetzli
2019-10-08Avoid printing success for `--force-logic` (#3363)Andres Noetzli
2019-06-21Fix and simplify handling of --force-logic (#3062)Andres Noetzli
2019-04-16Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)Andres Noetzli
2018-10-02Allow (_ to_fp ...) in strict parsing mode (#2566)Andres Noetzli
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-06-04Only enable transcendentals if logic is N[I]RAT (#2052)Andres Noetzli
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
2017-10-03Add regression from #50 regarding "as" parsing in smt2 (#1188)Andrew Reynolds
2016-11-17Fix Makefiles in testAndres Notzli
2015-01-14sygus input language and benchmarkMorgan Deters
2015-01-11adjusted to both v2.0 and v2.5 string literalsTianyi Liang
2015-01-09blocked unprintable characters in string literals;Tianyi Liang
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
2014-06-08test for prvs commit (tokenize emptyset)Kshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback