diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-05-14 15:36:52 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-14 15:36:52 -0700 |
| commit | 0c6681152ca422f7ace1bd1d3c3dac7823de2c14 (patch) | |
| tree | 84b7ab5df824cb26df70b437b6bb7ad41c30aadb /COPYING | |
| parent | b5264346e85bc7ca0235048f686cc252c60b0014 (diff) | |
Add contrib/get-symfpu for downloading symfpu. (#1905)
Diffstat (limited to 'COPYING')
| -rw-r--r-- | COPYING | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -79,6 +79,11 @@ licenses/lgpl-3.0.txt for a copy of that license. Note that according to the terms of the LGPL, both CVC4's source, and the combined work (CVC4 linked with GMP) may (and do) remain under the more permissive modified BSD license. +The implementation of the floating point solver in CVC4 depends on symfpu +(https://github.com/martin-cs/symfpu) written by Martin Brain. +See https://raw.githubusercontent.com/martin-cs/symfpu/CVC4/LICENSE for +copyright and licensing information. + CVC4 optionally links against the following libraries: ABC (https://bitbucket.org/alanmi/abc) |