mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
0e3fc3687f
* 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
6 lines
46 B
Plaintext
6 lines
46 B
Plaintext
|
|
unknown
|
|
(
|
|
(define-fun x () Real (/ 1 4))
|
|
)
|