mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
dc8087713d
* 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
5 lines
118 B
Plaintext
5 lines
118 B
Plaintext
logic x : real
|
|
|
|
axiom ax : 1.0 <= x
|
|
|
|
goal g : float(4, 4, NearestTiesToEven, 1.0) <= float(4, 4, NearestTiesToEven, x) |