summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fp
AgeCommit message (Expand)Author
2021-09-10FP: Do not send trivial lemmas. (#7167)Aina Niemetz
2021-07-29[proofs] Set BV solver to better proof-producing one when proofs on (#6903)Haniel Barbosa
2021-07-23FP: Add option to word-blast more lazily. (#6904)Aina Niemetz
2021-06-16Make symfpu a required dependency. (#6749)Aina Niemetz
2021-06-11Better support for HOL parsing and set up (#6697)Haniel Barbosa
2021-05-27Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)Andres Noetzli
2021-05-27Enable new justification heuristic by default (#6613)Andrew Reynolds
2021-05-07Fix and add missing REQUIRE labels for FP regression tests. (#6506)Aina Niemetz
2021-05-04FP: Move removal of generic to_fp operations to rewriter. (#6480)Aina Niemetz
2021-05-03FP: Rewrite to_fp conversion from signed bit-vector. (#6472)Aina Niemetz
2021-05-03SymFPU: Automatically apply patch from 2020-11-14. (#6471)Aina Niemetz
2021-04-24Improve getValue for non-evaluated operators (#6436)Andrew Reynolds
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2021-02-25Move slow regressions to regress1 (#5999)Andrew Reynolds
2020-12-17Simplify and fix check models (#5685)Andrew Reynolds
2020-12-02Fix RoundingMode mapping in API. (#5578)Aina Niemetz
2020-06-17Do not traverse WITNESS for partial substitutions in extended rewriter (#4630)Andrew Reynolds
2020-05-26Fix an incorrect limit in conversion from real to float (#4418)Martin
2020-04-14Always assign function values in higher order (#4279)Andrew Reynolds
2019-12-18Avoid calling rewriter from type checker (#3548)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-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-01-15 Fix unsound double abs rewrite rule for FP (#2792)Andrew Reynolds
2018-08-27Refactor extended rewriter, move rewrites to aggressive (#2387)Andrew Reynolds
2018-08-16Refactor extended rewriter preprocessing pass (#2324)Haniel Barbosa
2018-06-04Regressions: Support for requiring CVC4 features (#2044)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback