2 Commits

Author	SHA1	Message	Date
Pierrot	dc8087713d	Active fpa as default (#1177) ... * Activate FPA theory as default Activating FPA as default introduce a tiny time regression (about 1%) but we prove more goals on both `ae-format` and `why3-gallery`. Fix issue #917	2024-07-24 18:32:32 +02:00
Stevendeo	0e3fc3687f	feat: exporting alt-ergo FPA built-in primitives (#876) ... * Exporing rounding mode to SMT * Adding round as a non indexed primitive * Indexed identifier * Poetry * Adding some tests * Reverting Rounding Mode as index * Not relying on input format * Injecting AE type float rounding type into SMT rounding type * Poetry * Style * Poetry * More poetry * Also translating on the native side * Adding missing tests * Rebase artifact * Adding tests and some poetry	2023-10-30 16:42:22 +01:00